diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 06ff53d40e..e3d0265f23 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -1,6 +1,8 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField.Basic import LeanAPAP.Mathlib.Algebra.Group.AddChar +import LeanAPAP.Mathlib.Algebra.GroupWithZero.Units.Basic +import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Mathlib.Analysis.Complex.Circle import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index 8c67627f5f..0229b5056f 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -1,3 +1,5 @@ +import LeanAPAP.Mathlib.Algebra.GroupWithZero.Units.Basic +import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real import LeanAPAP.Mathlib.Data.Finset.Density import LeanAPAP.Mathlib.Data.Nat.Cast.Order.Basic @@ -12,7 +14,15 @@ import LeanAPAP.Physics.Unbalancing # Finite field case -/ -open FiniteDimensional Finset Fintype Function Real +namespace Real +variable {x : ℝ} + +lemma le_log_one_add_inv (hx : 0 < x) : (1 + x)⁻¹ ≤ log (1 + x⁻¹) := sorry + +end Real + +open FiniteDimensional Fintype Function Real +open Finset hiding card open scoped NNReal BigOperators Combinatorics.Additive Pointwise variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G] {A C : Finset G} {γ ε : ℝ} @@ -44,7 +54,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ) expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ← mul_inv_cancel₀, ← mul_sub, abs_mul, abs_of_nonneg, mul_div_cancel_left₀] <;> positivity · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow] - rw [cast_dens, le_div_iff, mul_comm] at hγC + rw [nnratCast_dens, le_div_iff, mul_comm] at hγC refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_) all_goals positivity · simp_rw [Nat.cast_mul, Nat.cast_two, p] @@ -132,48 +142,52 @@ lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.dens) (hγC sorry theorem ff (hq : 3 ≤ q) {A : Finset G} (hA₀ : A.Nonempty) (hA : ThreeAPFree (α := G) A) : - finrank (ZMod q) G ≤ curlog A.dens ^ 9 := by - obtain hα | hα := le_total (q ^ (finrank (ZMod q) G / 2 : ℝ) : ℝ) (2 * (A.dens : ℝ)⁻¹ ^ 2) + finrank (ZMod q) G ≤ 65 * curlog A.dens ^ 9 := by + let n : ℝ := finrank (ZMod q) G + let α : ℝ := A.dens + have : 1 < (q : ℝ) := mod_cast hq.trans_lt' (by norm_num) + have : 1 ≤ (q : ℝ) := this.le + have : 1 ≤ α⁻¹ := one_le_inv (by positivity) (by simp [α]) + have : 0 ≤ log α⁻¹ := log_nonneg ‹_› + have : 0 ≤ curlog α := curlog_nonneg (by positivity) (by simp [α]) + have : 0 < log q := log_pos ‹_› + obtain hα | hα := le_total (q ^ (n / 2) : ℝ) (2 * α⁻¹ ^ 2) · rw [rpow_le_iff_le_log, log_mul, log_pow, Nat.cast_two, ← mul_div_right_comm, mul_div_assoc, ← le_div_iff] at hα calc - _ ≤ (log 2 + 2 * log A.dens⁻¹) / (log q / 2) := hα - _ = 4 / log q * (log A.dens⁻¹ + log 2 / 2) := by ring - _ ≤ (0 + 2) ^ 8 * (log A.dens⁻¹ + 2) := by + _ ≤ (log 2 + 2 * log α⁻¹) / (log q / 2) := hα + _ = 4 / log q * (log α⁻¹ + log 2 / 2) := by ring + _ ≤ 65 * (0 + 2) ^ 8 * (log α⁻¹ + 2) := by gcongr - · exact add_nonneg (log_nonneg $ one_le_inv (by positivity) (mod_cast dens_le_one)) - (div_nonneg (log_nonneg (by norm_num)) (by norm_num)) · calc 4 / log q ≤ 4 / log 3 := by gcongr; assumption_mod_cast _ ≤ 4 / log 2 := by gcongr; norm_num _ ≤ 4 / 0.6931471803 := by gcongr; exact log_two_gt_d9.le - _ ≤ (0 + 2) ^ 8 := by norm_num + _ ≤ 65 * (0 + 2) ^ 8 := by norm_num · calc log 2 / 2 ≤ 0.6931471808 / 2 := by gcongr; exact log_two_lt_d9.le _ ≤ 2 := by norm_num - _ ≤ (log A.dens⁻¹ + 2) ^ 8 * (log A.dens⁻¹ + 2) := by - gcongr - sorry - sorry - _ = curlog A.dens ^ 9 := by rw [curlog_eq_log_inv_add_two, pow_succ _ 8]; positivity - any_goals positivity - sorry + _ ≤ 65 * (log α⁻¹ + 2) ^ 8 * (log α⁻¹ + 2) := by gcongr + _ = 65 * curlog α ^ 9 := by + rw [curlog_eq_log_inv_add_two, pow_succ _ 8, mul_assoc]; positivity + all_goals positivity have ind (i : ℕ) : ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)) (B : Finset V) (x : G), - finrank (ZMod q) G ≤ finrank (ZMod q) V + i * curlog A.dens ^ 8 ∧ ThreeAPFree (B : Set V) ∧ - A.dens ≤ B.dens ∧ - (B.dens < (65 / 64 : ℝ) ^ i * A.dens → + n ≤ finrank (ZMod q) V + i * curlog α ^ 8 ∧ ThreeAPFree (B : Set V) ∧ + α ≤ B.dens ∧ + (B.dens < (65 / 64 : ℝ) ^ i * α → 2⁻¹ ≤ card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by induction' i with i ih hi · exact ⟨⊤, Classical.decPred _, A.map (Equiv.subtypeUnivEquiv (by simp)).symm.toEmbedding, 0, by simp, sorry, by simp, - by simp [cast_dens, Fintype.card_subtype, subset_iff]⟩ + by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩ obtain ⟨V, _, B, x, hV, hB, hαβ, hBV⟩ := ih obtain hB' | hB' := le_or_lt 2⁻¹ (card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) · exact ⟨V, inferInstance, B, x, hV.trans (by gcongr; exact i.le_succ), hB, hαβ, fun _ ↦ hB'⟩ sorry -- have := di_in_ff (by positivity) one_half_lt_one _ _ _ _ - obtain ⟨V, _, B, x, hV, hB, hαβ, hBV⟩ := ind ⌊curlog A.dens / log (65 / 64)⌋₊ + obtain ⟨V, _, B, x, hV, hB, hαβ, hBV⟩ := ind ⌊curlog α / log (65 / 64)⌋₊ + let β : ℝ := B.dens have aux : 0 < log (65 / 64) := log_pos (by norm_num) specialize hBV $ by calc @@ -181,12 +195,12 @@ theorem ff (hq : 3 ≤ q) {A : Finset G} (hA₀ : A.Nonempty) (hA : ThreeAPFree _ < _ := ?_ rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff] calc - log A.dens⁻¹ / log (65 / 64) - < ⌊log A.dens⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _ - _ = ⌊(log A.dens⁻¹ + log (65 / 64)) / log (65 / 64)⌋₊ := by + log α⁻¹ / log (65 / 64) + < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _ + _ = ⌊(log α⁻¹ + log (65 / 64)) / log (65 / 64)⌋₊ := by rw [← div_add_one aux.ne', Nat.floor_add_one, Nat.cast_succ] - exact div_nonneg (log_nonneg $ one_le_inv (by positivity) (by simp)) aux.le - _ ≤ ⌊curlog A.dens / log (65 / 64)⌋₊ := by + exact div_nonneg (log_nonneg $ one_le_inv (by positivity) (by simp [α])) aux.le + _ ≤ ⌊curlog α / log (65 / 64)⌋₊ := by rw [curlog_eq_log_inv_add_two] gcongr · calc @@ -196,5 +210,28 @@ theorem ff (hq : 3 ≤ q) {A : Finset G} (hA₀ : A.Nonempty) (hA : ThreeAPFree · positivity all_goals positivity rw [hB.l2Inner_mu_conv_mu_mu_two_smul_mu] at hBV + have : (q ^ (n - 65 * curlog α ^ 9) : ℝ) ≤ q ^ (n / 2) := + calc + _ ≤ ↑q ^ (finrank (ZMod q) V : ℝ) := by + gcongr + · assumption + rw [sub_le_comm] + calc + n - finrank (ZMod q) V ≤ ⌊curlog α / log (65 / 64)⌋₊ * curlog α ^ 8 := by + rwa [sub_le_iff_le_add'] + _ ≤ curlog α / log (65 / 64) * curlog α ^ 8 := by + gcongr; exact Nat.floor_le (by positivity) + _ = (log (65 / 64)) ⁻¹ * curlog α ^ 9 := by ring + _ ≤ _ := by + gcongr + sorry + _ = ↑(card V) := sorry + _ ≤ 2 * β⁻¹ ^ 2 := by + rw [← natCast_card_mul_nnratCast_dens, mul_pow, mul_inv, ← mul_assoc, + ← div_eq_mul_inv (card V : ℝ), ← zpow_one_sub_natCast₀ (by positivity)] at hBV + have : 0 < (card V : ℝ) := by positivity + simpa [le_mul_inv_iff₀', inv_mul_le_iff₀', this, zero_lt_two, mul_comm] using hBV + _ ≤ 2 * α⁻¹ ^ 2 := by gcongr + _ ≤ _ := hα sorry sorry diff --git a/LeanAPAP/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/LeanAPAP/Mathlib/Algebra/GroupWithZero/Units/Basic.lean new file mode 100644 index 0000000000..9e71b7e38e --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/GroupWithZero/Units/Basic.lean @@ -0,0 +1,12 @@ +import Mathlib.Algebra.GroupWithZero.Units.Basic + +variable {G₀ : Type*} [GroupWithZero G₀] {a : G₀} + +lemma zpow_natCast_sub_natCast₀ (ha : a ≠ 0) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n := by + rw [zpow_sub₀ ha, zpow_natCast, zpow_natCast] + +lemma zpow_natCast_sub_one₀ (ha : a ≠ 0) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a := by + simpa using zpow_natCast_sub_natCast₀ ha n 1 + +lemma zpow_one_sub_natCast₀ (ha : a ≠ 0) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n := by + simpa using zpow_natCast_sub_natCast₀ ha 1 n diff --git a/LeanAPAP/Mathlib/Algebra/Order/Group/Unbundled/Basic.lean b/LeanAPAP/Mathlib/Algebra/Order/Group/Unbundled/Basic.lean new file mode 100644 index 0000000000..6805c47487 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Order/Group/Unbundled/Basic.lean @@ -0,0 +1,5 @@ +/-! +# TODO + +Rename `le_mul_inv_iff_mul_le` to `le_mul_inv_iff` +-/ diff --git a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean index 7e0487753b..528b77d923 100644 --- a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean +++ b/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean @@ -1,18 +1,235 @@ +import Mathlib.Algebra.Group.Pi.Basic +import Mathlib.Algebra.GroupWithZero.Basic import Mathlib.Algebra.Order.GroupWithZero.Unbundled +import Mathlib.Algebra.Order.ZeroLEOne +import Mathlib.Tactic.Nontriviality -section LinearOrderedSemiring -variable {G₀ : Type*} [Zero G₀] [MulOneClass G₀] [Preorder G₀] {a b : G₀} +variable {α M₀ G₀ : Type*} -lemma one_lt_of_lt_mul_left₀ [PosMulReflectLT G₀] (ha : 0 ≤ a) (h : a < a * b) : 1 < b := +section MulOneClass +variable [Zero M₀] [MulOneClass M₀] [Preorder M₀] {a b : M₀} + +lemma one_lt_of_lt_mul_left₀ [PosMulReflectLT M₀] (ha : 0 ≤ a) (h : a < a * b) : 1 < b := lt_of_mul_lt_mul_left (by simpa) ha -lemma one_lt_of_lt_mul_right₀ [MulPosReflectLT G₀] (hb : 0 ≤ b) (h : b < a * b) : 1 < a := +lemma one_lt_of_lt_mul_right₀ [MulPosReflectLT M₀] (hb : 0 ≤ b) (h : b < a * b) : 1 < a := lt_of_mul_lt_mul_right (by simpa) hb -lemma one_le_of_le_mul_left₀ [PosMulReflectLE G₀] (ha : 0 < a) (h : a ≤ a * b) : 1 ≤ b := +lemma one_le_of_le_mul_left₀ [PosMulReflectLE M₀] (ha : 0 < a) (h : a ≤ a * b) : 1 ≤ b := le_of_mul_le_mul_left (by simpa) ha -lemma one_le_of_le_mul_right₀ [MulPosReflectLE G₀] (hb : 0 < b) (h : b ≤ a * b) : 1 ≤ a := +lemma one_le_of_le_mul_right₀ [MulPosReflectLE M₀] (hb : 0 < b) (h : b ≤ a * b) : 1 ≤ a := le_of_mul_le_mul_right (by simpa) hb -end LinearOrderedSemiring +end MulOneClass + +section MonoidWithZero +variable [MonoidWithZero M₀] + +section Preorder +variable [Preorder M₀] {a b c d : M₀} + +@[simp] lemma pow_nonneg' [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 0 ≤ a) : ∀ n, 0 ≤ a ^ n + | 0 => pow_zero a ▸ zero_le_one + | n + 1 => pow_succ a n ▸ mul_nonneg (pow_nonneg' ha _) ha + +lemma pow_le_pow_of_le_one'' [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha₀ : 0 ≤ a) + (ha₁ : a ≤ 1) : ∀ {m n : ℕ}, m ≤ n → a ^ n ≤ a ^ m + | _, _, Nat.le.refl => le_rfl + | _, _, Nat.le.step h => by + rw [pow_succ'] + exact (mul_le_of_le_one_left (pow_nonneg' ha₀ _) ha₁).trans <| pow_le_pow_of_le_one'' ha₀ ha₁ h + +lemma pow_le_of_le_one' [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] + (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ a := + (pow_one a).subst (pow_le_pow_of_le_one'' h₀ h₁ (Nat.pos_of_ne_zero hn)) + +lemma sq_le' [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : + a ^ 2 ≤ a := pow_le_of_le_one' h₀ h₁ two_ne_zero + +lemma one_le_mul_of_one_le_of_one_le' [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) + (hb : 1 ≤ b) : (1 : M₀) ≤ a * b := + Left.one_le_mul_of_le_of_le ha hb <| zero_le_one.trans ha + +lemma mul_le_one'' [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : a ≤ 1) (hb' : 0 ≤ b) + (hb : b ≤ 1) : a * b ≤ 1 := one_mul (1 : M₀) ▸ mul_le_mul ha hb hb' zero_le_one + +lemma one_lt_mul_of_le_of_lt'' [ZeroLEOneClass M₀] [MulPosMono M₀] (ha : 1 ≤ a) (hb : 1 < b) : + 1 < a * b := hb.trans_le <| le_mul_of_one_le_left (zero_le_one.trans hb.le) ha + +lemma one_lt_mul_of_lt_of_le'' [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 < a) (hb : 1 ≤ b) : + 1 < a * b := ha.trans_le <| le_mul_of_one_le_right (zero_le_one.trans ha.le) hb + +alias one_lt_mul''' := one_lt_mul_of_le_of_lt'' + +lemma mul_lt_one_of_nonneg_of_lt_one_left' [PosMulMono M₀] (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) : + a * b < 1 := (mul_le_of_le_one_right ha₀ hb).trans_lt ha + +lemma mul_lt_one_of_nonneg_of_lt_one_right' [MulPosMono M₀] (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) : + a * b < 1 := (mul_le_of_le_one_left hb₀ ha).trans_lt hb + +variable [Preorder α] {f g : α → M₀} + +lemma monotone_mul_left_of_nonneg' [PosMulMono M₀] (ha : 0 ≤ a) : Monotone fun x ↦ a * x := + fun _ _ h ↦ mul_le_mul_of_nonneg_left h ha + +lemma monotone_mul_right_of_nonneg' [MulPosMono M₀] (ha : 0 ≤ a) : Monotone fun x ↦ x * a := + fun _ _ h ↦ mul_le_mul_of_nonneg_right h ha + +lemma Monotone.mul_const'' [MulPosMono M₀] (hf : Monotone f) (ha : 0 ≤ a) : + Monotone fun x ↦ f x * a := (monotone_mul_right_of_nonneg' ha).comp hf + +lemma Monotone.const_mul'' [PosMulMono M₀] (hf : Monotone f) (ha : 0 ≤ a) : + Monotone fun x ↦ a * f x := (monotone_mul_left_of_nonneg' ha).comp hf + +lemma Antitone.mul_const'' [MulPosMono M₀] (hf : Antitone f) (ha : 0 ≤ a) : + Antitone fun x ↦ f x * a := (monotone_mul_right_of_nonneg' ha).comp_antitone hf + +lemma Antitone.const_mul'' [PosMulMono M₀] (hf : Antitone f) (ha : 0 ≤ a) : + Antitone fun x ↦ a * f x := (monotone_mul_left_of_nonneg' ha).comp_antitone hf + +lemma Monotone.mul'' [PosMulMono M₀] [MulPosMono M₀] (hf : Monotone f) (hg : Monotone g) + (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 ≤ g x) : Monotone (f * g) := + fun _ _ h ↦ mul_le_mul (hf h) (hg h) (hg₀ _) (hf₀ _) + +end Preorder + + +section PartialOrder +variable [PartialOrder M₀] {a b c d : M₀} + +@[simp] lemma pow_pos' [ZeroLEOneClass M₀] [PosMulStrictMono M₀] (ha : 0 < a) : ∀ n, 0 < a ^ n + | 0 => by nontriviality; rw [pow_zero]; exact zero_lt_one + | n + 1 => pow_succ a _ ▸ mul_pos (pow_pos' ha _) ha + +lemma mul_self_lt_mul_self' [PosMulStrictMono M₀] [MulPosMono M₀] (ha : 0 ≤ a) (hab : a < b) : + a * a < b * b := mul_lt_mul' hab.le hab ha <| ha.trans_lt hab + +-- In the next lemma, we used to write `Set.Ici 0` instead of `{x | 0 ≤ x}`. +-- As this lemma is not used outside this file, +-- and the import for `Set.Ici` is not otherwise needed until later, +-- we choose not to use it here. +lemma strictMonoOn_mul_self' [PosMulStrictMono M₀] [MulPosMono M₀] : + StrictMonoOn (fun x ↦ x * x) {x : M₀ | 0 ≤ x} := fun _ hx _ _ hxy ↦ mul_self_lt_mul_self' hx hxy + +-- See Note [decidable namespace] +protected lemma Decidable.mul_lt_mul''' [PosMulMono M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] + [@DecidableRel M₀ (· ≤ ·)] (h1 : a < c) (h2 : b < d) + (h3 : 0 ≤ a) (h4 : 0 ≤ b) : a * b < c * d := + h4.lt_or_eq_dec.elim (fun b0 ↦ mul_lt_mul h1 h2.le b0 <| h3.trans h1.le) fun b0 ↦ by + rw [← b0, mul_zero]; exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2) + +lemma lt_mul_left' [MulPosStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < b * a := by + simpa using mul_lt_mul_of_pos_right hb ha + +lemma lt_mul_right' [PosMulStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < a * b := by + simpa using mul_lt_mul_of_pos_left hb ha + +lemma lt_mul_self' [ZeroLEOneClass M₀] [MulPosStrictMono M₀] (ha : 1 < a) : a < a * a := + lt_mul_left' (ha.trans_le' zero_le_one) ha + +variable [Preorder α] {f g : α → M₀} + +lemma strictMono_mul_left_of_pos' [PosMulStrictMono M₀] (ha : 0 < a) : + StrictMono fun x ↦ a * x := fun _ _ b_lt_c ↦ mul_lt_mul_of_pos_left b_lt_c ha + +lemma strictMono_mul_right_of_pos' [MulPosStrictMono M₀] (ha : 0 < a) : + StrictMono fun x ↦ x * a := fun _ _ b_lt_c ↦ mul_lt_mul_of_pos_right b_lt_c ha + +lemma StrictMono.mul_const'' [MulPosStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) : + StrictMono fun x ↦ f x * a := (strictMono_mul_right_of_pos' ha).comp hf + +lemma StrictMono.const_mul'' [PosMulStrictMono M₀] (hf : StrictMono f) (ha : 0 < a) : + StrictMono fun x ↦ a * f x := (strictMono_mul_left_of_pos' ha).comp hf + +lemma StrictAnti.mul_const'' [MulPosStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) : + StrictAnti fun x ↦ f x * a := (strictMono_mul_right_of_pos' ha).comp_strictAnti hf + +lemma StrictAnti.const_mul'' [PosMulStrictMono M₀] (hf : StrictAnti f) (ha : 0 < a) : + StrictAnti fun x ↦ a * f x := (strictMono_mul_left_of_pos' ha).comp_strictAnti hf + +lemma StrictMono.mul_monotone'' [PosMulMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) + (hg : Monotone g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 < g x) : + StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul (hf h) (hg h.le) (hg₀ _) (hf₀ _) + +lemma Monotone.mul_strictMono'' [PosMulStrictMono M₀] [MulPosMono M₀] (hf : Monotone f) + (hg : StrictMono g) (hf₀ : ∀ x, 0 < f x) (hg₀ : ∀ x, 0 ≤ g x) : + StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul' (hf h.le) (hg h) (hg₀ _) (hf₀ _) + +lemma StrictMono.mul'' [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hf : StrictMono f) + (hg : StrictMono g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 ≤ g x) : + StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul'' (hf h) (hg h) (hf₀ _) (hg₀ _) + +end MonoidWithZero.PartialOrder + +section GroupWithZero +variable {G₀ : Type*} [GroupWithZero G₀] + +section PartialOrder +variable [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} + +-- TODO: Replace `inv_pos` +@[simp] lemma inv_pos' : 0 < a⁻¹ ↔ 0 < a := + suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩ + fun a ha ↦ flip lt_of_mul_lt_mul_left ha.le <| by simp [ne_of_gt ha, zero_lt_one] + +alias ⟨_, inv_pos_of_pos'⟩ := inv_pos' + +@[simp] lemma inv_nonneg' : 0 ≤ a⁻¹ ↔ 0 ≤ a := by simp only [le_iff_eq_or_lt, inv_pos', zero_eq_inv] + +alias ⟨_, inv_nonneg_of_nonneg'⟩ := inv_nonneg' + +lemma one_div_pos' : 0 < 1 / a ↔ 0 < a := one_div a ▸ inv_pos' +lemma one_div_nonneg' : 0 ≤ 1 / a ↔ 0 ≤ a := one_div a ▸ inv_nonneg' + +lemma div_pos' [PosMulStrictMono G₀] (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by + rw [div_eq_mul_inv]; exact mul_pos ha (inv_pos'.2 hb) + +lemma div_nonneg' [PosMulMono G₀] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by + rw [div_eq_mul_inv]; exact mul_nonneg ha (inv_nonneg'.2 hb) + +lemma div_nonpos_of_nonpos_of_nonneg' [MulPosMono G₀] (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0 := by + rw [div_eq_mul_inv]; exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg'.2 hb) + +lemma zpow_nonneg' [PosMulMono G₀] (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n + | (n : ℕ) => by rw [zpow_natCast]; exact pow_nonneg' ha _ + |-(n + 1 : ℕ) => by rw [zpow_neg, inv_nonneg', zpow_natCast]; exact pow_nonneg' ha _ + +lemma zpow_pos_of_pos' [PosMulStrictMono G₀] (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n + | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos' ha _ + |-(n + 1 : ℕ) => by rw [zpow_neg, inv_pos', zpow_natCast]; exact pow_pos' ha _ + +lemma le_inv_mul_iff₀' [PosMulMono G₀] [MulPosMono G₀] (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b where + mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h hc.le + mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h (inv_nonneg'.2 hc.le) + +-- TODO: Replace `le_mul_inv_iff₀` +lemma le_mul_inv_iff₀' [PosMulMono G₀] [MulPosMono G₀] (hc : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b where + mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h hc.le + mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg'.2 hc.le) + +lemma inv_mul_le_iff₀' [PosMulMono G₀] [MulPosMono G₀] (hc : 0 < c) : c⁻¹ * b ≤ a ↔ b ≤ c * a where + mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h hc.le + mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_left h (inv_nonneg'.2 hc.le) + +-- TODO: Replace `le_mul_inv_iff₀` +lemma mul_inv_le_iff₀' [PosMulMono G₀] [MulPosMono G₀] (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ a * c where + mp h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h hc.le + mpr h := by simpa [hc.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg'.2 hc.le) + +end PartialOrder + +section LinearOrder +variable [LinearOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] {a b c : G₀} + +@[simp] lemma inv_neg'' : a⁻¹ < 0 ↔ a < 0 := by simp only [← not_le, inv_nonneg'] + +@[simp] lemma inv_nonpos' : a⁻¹ ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, inv_pos'] + +lemma one_div_neg' : 1 / a < 0 ↔ a < 0 := one_div a ▸ inv_neg'' +lemma one_div_nonpos' : 1 / a ≤ 0 ↔ a ≤ 0 := one_div a ▸ inv_nonpos' + +lemma div_nonpos_of_nonneg_of_nonpos' [PosMulMono G₀] (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0 := by + rw [div_eq_mul_inv]; exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos'.2 hb) + +end GroupWithZero.LinearOrder diff --git a/LeanAPAP/Mathlib/Data/Finset/Density.lean b/LeanAPAP/Mathlib/Data/Finset/Density.lean index 523e91d312..265e43ce0d 100644 --- a/LeanAPAP/Mathlib/Data/Finset/Density.lean +++ b/LeanAPAP/Mathlib/Data/Finset/Density.lean @@ -4,17 +4,36 @@ import Mathlib.Data.Rat.Cast.CharZero open Fintype namespace Finset -variable {α β 𝕜 : Type*} [Fintype α][Fintype β] {s : Finset α} +variable {α β 𝕜 : Type*} [Fintype α] [Fintype β] {s : Finset α} + +lemma card_mul_dens (s : Finset α) : Fintype.card α * s.dens = s.card := by + cases isEmpty_or_nonempty α + · simp [Subsingleton.elim s ∅] + rw [dens, mul_div_cancel₀] + exact mod_cast Fintype.card_ne_zero + +lemma dens_mul_card (s : Finset α) : s.dens * Fintype.card α = s.card := by + rw [mul_comm, card_mul_dens] @[simp] lemma dens_le_one : s.dens ≤ 1 := by cases isEmpty_or_nonempty α · simp [Subsingleton.elim s ∅] · simpa using dens_le_dens s.subset_univ -lemma cast_dens [Semifield 𝕜] [CharZero 𝕜] (s : Finset α) : - (s.dens : 𝕜) = s.card / Fintype.card α := by simp [dens] - @[simp] lemma dens_map_equiv (e : α ≃ β) : (Finset.map e.toEmbedding s).dens = s.dens := by simp [dens, Fintype.card_congr e] +section Semifield +variable [Semifield 𝕜] [CharZero 𝕜] + +lemma natCast_card_mul_nnratCast_dens (s : Finset α) : (Fintype.card α * s.dens : 𝕜) = s.card := + mod_cast s.card_mul_dens + +lemma nnratCast_dens_mul_natCast_card (s : Finset α) : s.dens * Fintype.card α = s.card := + mod_cast s.dens_mul_card + +@[norm_cast] lemma nnratCast_dens (s : Finset α) : (s.dens : 𝕜) = s.card / Fintype.card α := by + simp [dens] + +end Semifield end Finset diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index d7bf60b09c..7e09724308 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -237,7 +237,7 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p 4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / A.card ^ (2 * p) := by rw [mul_div_assoc, ← div_pow] refine mul_le_mul_of_nonneg_left (pow_le_pow_left (by positivity) ?_ _) (by norm_num) - rw [cast_dens, le_div_iff, ← mul_div_right_comm] + rw [nnratCast_dens, le_div_iff, ← mul_div_right_comm] calc _ = ‖𝟭_[ℝ] A ○ 𝟭 A‖_[1, μ univ] := by simp [mu, wlpNorm_smul_right, hp₀, l1Norm_dconv, card_univ, inv_mul_eq_div] @@ -245,5 +245,5 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p · exact Nat.cast_pos.2 hA.card_pos obtain ⟨A₁, -, A₂, -, h, hcard₁, hcard₂⟩ := sifting univ univ hε hε₁ hδ hp hp₂ hpε (by simp [univ_nonempty]) hA (by simpa) - exact ⟨A₁, A₂, h, this.trans $ by simpa [cast_dens] using hcard₁, - this.trans $ by simpa [cast_dens] using hcard₂⟩ + exact ⟨A₁, A₂, h, this.trans $ by simpa [nnratCast_dens] using hcard₁, + this.trans $ by simpa [nnratCast_dens] using hcard₂⟩