diff --git a/LeanAPAP.lean b/LeanAPAP.lean index b34e17bff4..30bdae363b 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -2,7 +2,6 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField.Basic import LeanAPAP.Mathlib.Algebra.Group.AddChar import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic -import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Mathlib.Analysis.RCLike.Basic import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean index b760187701..a4959905df 100644 --- a/LeanAPAP/Extras/BSG.lean +++ b/LeanAPAP/Extras/BSG.lean @@ -286,7 +286,7 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K) refine h.le.trans ?_ rw [mul_assoc] gcongr _ * ?_ - field_simp [hA, hB, hK, le_div_iff, div_le_iff] at hE ⊢ + field_simp [hA, hB, hK, le_div_iff₀, div_le_iff₀] at hE ⊢ convert_to (A.card ^ 2 * B.card) ^ 2 ≤ (E[A, B] * K) ^ 2 · ring_nf · ring_nf @@ -407,8 +407,8 @@ theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < A.card) (hB : (0 : ℝ) · rw [← mul_inv, inv_mul_eq_div] exact oneOfPair_bound (filter_subset _ _) this (hX₃.trans_eq' (by norm_num)) hX₂ have := big_quadruple_bound (H := H) (fun x hx ↦ (mem_filter.1 hx).2) (filter_subset _ _) hX₂ - rw [le_div_iff (by positivity)] - rw [mul_div_assoc', div_le_iff (by positivity)] at this + rw [le_div_iff₀ (by positivity)] + rw [mul_div_assoc', div_le_iff₀ (by positivity)] at this exact this.trans_eq (by ring) theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) : diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index 930e33995d..64980c0219 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -1,6 +1,4 @@ -import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic -import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real import LeanAPAP.Mathlib.Data.Rat.Cast.Order import LeanAPAP.Prereqs.Convolution.ThreeAP import LeanAPAP.Prereqs.FourierTransform.Compact @@ -30,7 +28,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ) Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ hγ₁) have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one $ mod_cast hp have hp'' : (p : ℝ≥0).IsConjExponent _ := .conjExponent $ mod_cast hp - rw [mul_comm, ← div_div, div_le_iff (zero_lt_two' ℝ)] + rw [mul_comm, ← div_div, div_le_iff₀ (zero_lt_two' ℝ)] calc _ ≤ _ := div_le_div_of_nonneg_right hAC (card G).cast_nonneg _ = |⟪balance (μ A) ∗ balance (μ A), μ C⟫_[ℝ]| := ?_ @@ -46,7 +44,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 [nnratCast_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] @@ -128,7 +126,7 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε < -- mul_inv_cancel₀ (show (card G : ℝ) ≠ 0 by positivity)] · have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈γ.curlog⌉₊ := sorry sorry - -- simpa [wlpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity), + -- simpa [wlpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff₀' (show (0 : ℝ) < card G by positivity), -- ← div_div, *] using global_dichotomy hA hγC hγ hAC sorry @@ -148,7 +146,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) 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α + mul_div_assoc, ← le_div_iff₀] at hα calc _ ≤ (log 2 + 2 * log α⁻¹) / (log q / 2) := hα _ = 4 / log q * (log α⁻¹ + log 2 / 2) := by ring @@ -213,7 +211,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) all_goals positivity rw [hB.l2Inner_mu_conv_mu_mu_two_smul_mu] at hBV suffices h : (q ^ (n - 65 * curlog α ^ 9) : ℝ) ≤ q ^ (n / 2) by - rw [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff' zero_lt_two, ← mul_assoc] at h + rw [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff₀' zero_lt_two, ← mul_assoc] at h norm_num at h exact h calc @@ -239,7 +237,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) 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_inv_mul_iff₀', mul_inv_le_iff₀', this, zero_lt_two, mul_comm] using hBV + simpa [le_inv_mul_iff₀, mul_inv_le_iff₀, this, zero_lt_two, mul_comm] using hBV _ ≤ 2 * α⁻¹ ^ 2 := by gcongr _ ≤ _ := hα simpa [card_eq_pow_finrank (K := ZMod q) (V := V), ZMod.card] using hq'.pow diff --git a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean deleted file mode 100644 index 528b77d923..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean +++ /dev/null @@ -1,235 +0,0 @@ -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 - -variable {α M₀ G₀ : Type*} - -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 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 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 M₀] (hb : 0 < b) (h : b ≤ a * b) : 1 ≤ a := - le_of_mul_le_mul_right (by simpa) hb - -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/Analysis/SpecialFunctions/Log/Basic.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index 03c2280e6b..f28c08842b 100644 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -1,5 +1,4 @@ import Mathlib.Analysis.SpecialFunctions.Log.Basic -import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled namespace Real variable {x : ℝ} diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean index 440c292d34..901df46926 100644 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean @@ -3,36 +3,6 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Real namespace Real variable {x y z : ℝ} -lemma rpow_le_iff_le_log (hx : 0 < x) (hy : 0 < y) : x ^ z ≤ y ↔ z * log x ≤ log y := by - rw [← log_le_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx] - -lemma rpow_lt_iff_lt_log (hx : 0 < x) (hy : 0 < y) : x ^ z < y ↔ z * log x < log y := by - rw [← log_lt_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx] - -lemma pow_le_iff_le_log {n : ℕ} (hx : 0 < x) (hy : 0 < y) : - x ^ n ≤ y ↔ n * log x ≤ log y := by rw [← rpow_le_iff_le_log hx hy, rpow_natCast] - -lemma zpow_le_iff_le_log {n : ℤ} (hx : 0 < x) (hy : 0 < y) : - x ^ n ≤ y ↔ n * log x ≤ log y := by rw [← rpow_le_iff_le_log hx hy, rpow_intCast] - -lemma pow_lt_iff_lt_log {n : ℕ} (hx : 0 < x) (hy : 0 < y) : - x ^ n < y ↔ n * log x < log y := by rw [← rpow_lt_iff_lt_log hx hy, rpow_natCast] - -lemma zpow_lt_iff_lt_log {n : ℤ} (hx : 0 < x) (hy : 0 < y) : - x ^ n < y ↔ n * log x < log y := by rw [← rpow_lt_iff_lt_log hx hy, rpow_intCast] - -lemma le_pow_iff_log_le {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ n ↔ log x ≤ n * log y := by - rw [← le_rpow_iff_log_le hx hy, rpow_natCast] - -lemma le_zpow_iff_log_le {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ n ↔ log x ≤ n * log y := by - rw [← le_rpow_iff_log_le hx hy, rpow_intCast] - -lemma lt_pow_iff_log_lt {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x < y ^ n ↔ log x < n * log y := by - rw [← lt_rpow_iff_log_lt hx hy, rpow_natCast] - -lemma lt_zpow_iff_log_lt {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x < y ^ n ↔ log x < n * log y := by - rw [← lt_rpow_iff_log_lt hx hy, rpow_intCast] - -- TODO: Replace in mathlib alias rpow_add_intCast := rpow_add_int alias rpow_add_natCast := rpow_add_nat diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index 53374e7edf..e0a1f5e53b 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -110,8 +110,8 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) : refine pow_le_pow_left (by positivity) ?_ _ rw [mul_right_comm, mul_comm _ ε, mul_pow, ← mul_assoc, sq (k : ℝ), ← mul_assoc] refine mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg k) - rw [mul_right_comm, div_mul_eq_mul_div, one_mul, div_mul_eq_mul_div, le_div_iff' (zero_lt_two' ℝ), - ← div_le_iff', ← mul_assoc] + rw [mul_right_comm, div_mul_eq_mul_div, one_mul, div_mul_eq_mul_div, le_div_iff₀' (zero_lt_two' ℝ), + ← div_le_iff₀', ← mul_assoc] · norm_num1; exact hk positivity @@ -337,7 +337,7 @@ lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) * have : (0 : ℝ) < Ac ^ k := by positivity refine le_of_mul_le_mul_left ?_ this have : (Ac : ℝ) ^ k ≤ K * Lc := by - rw [div_le_iff'] at h₂ + rw [div_le_iff₀'] at h₂ refine h₂.trans (mul_le_mul_of_nonneg_right hK' (Nat.cast_nonneg _)) exact zero_lt_two rw [neg_mul, neg_div, Real.rpow_neg hK.le, mul_left_comm, diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 8939f73ed3..479c196a8f 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -101,7 +101,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ positivity have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) ≤ (A₁ s).card / B₁.card * ((A₂ s).card / B₂.card) := by - rw [div_mul_div_comm, le_div_iff] + rw [div_mul_div_comm, le_div_iff₀] simpa [hg_def, hM_def, mul_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num, mul_div_right_comm] using h positivity @@ -188,11 +188,11 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 _ = ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_ _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by simp [l2Inner_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply] - _ ≤ _ := (le_div_iff $ lpNorm_conv_pos hp₀.ne' hB hA).2 h + _ ≤ _ := (le_div_iff₀ $ lpNorm_conv_pos hp₀.ne' hB hA).2 h _ ≤ _ := ?_ · simp_rw [sub_eq_iff_eq_add', sum_add_sum_compl, sum_dconv, map_mu] rw [sum_mu _ hA₁, sum_mu _ hA₂, one_mul] - rw [div_le_iff (lpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff' (zero_lt_two' ℝ)] + rw [div_le_iff₀ (lpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff₀' (zero_lt_two' ℝ)] simp only [apply_ite NNReal.toReal, indicate_apply, NNReal.coe_one, NNReal.coe_zero, mul_boole, sum_ite_mem, univ_inter, mul_div_right_comm] calc @@ -236,7 +236,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 [nnratCast_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] diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index c097c287a2..2867d48e32 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -144,7 +144,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 set p' := 24 / ε * log (3 / ε) * p have hp' : 0 < p' := p'_pos hp hε₀ hε₁ have : 1 - 8⁻¹ * ε ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ := by - rw [← div_le_iff, mul_div_assoc, ← div_pow, le_sqrt, mul_pow, ← pow_mul'] at this + rw [← div_le_iff₀, mul_div_assoc, ← div_pow, le_sqrt, mul_pow, ← pow_mul'] at this calc _ ≤ exp (-(8⁻¹ * ε)) := one_sub_le_exp_neg _ _ = ((ε / 3) ^ p * (ε / 3) ^ (2 * p)) ^ p'⁻¹ := ?_ diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index 4a2820dc1c..36b6644865 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -76,7 +76,7 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x sum_mul_sq_le_sq_mul_sq _ _ _ _ ≤ ‖f‖_[2] ^ 2 * ∑ x, ν x * (‖∑ γ in Δ, c γ * conj (γ x)‖ ^ 2) ^ m := by simp_rw [l2Norm_sq_eq_sum, mul_pow, sq_sqrt (NNReal.coe_nonneg _), pow_right_comm]; rfl - rw [mul_rotate', mul_left_comm, mul_pow, mul_pow, ← pow_mul', ← pow_mul', ← div_le_iff', + rw [mul_rotate', mul_left_comm, mul_pow, mul_pow, ← pow_mul', ← pow_mul', ← div_le_iff₀', mul_div_assoc, mul_div_assoc] at this calc _ ≤ _ := this @@ -100,7 +100,7 @@ lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) ↑Δ.card ^ (2 * m) * (η ^ (2 * m) * α f) ≤ boringEnergy m Δ := by have hG : (0 : ℝ) < card G := by positivity simpa [boringEnergy, α, mul_assoc, ← Pi.one_def, ← mul_div_right_comm, ← mul_div_assoc, - div_le_iff hG, energy_nsmul, -nsmul_eq_mul, ← nsmul_eq_mul'] using + div_le_iff₀ hG, energy_nsmul, -nsmul_eq_mul, ← nsmul_eq_mul'] using general_hoelder hη 1 (fun (_ : G) _ ↦ le_rfl) hΔ hm noncomputable def changConst : ℝ := 32 * exp 1 diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index 8033bb2053..651afa53ab 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -226,7 +226,7 @@ theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a _ ≤ (4 * ↑(m + 1)) ^ (m + 1) * n ^ m * ∑ a in A ^^ n, ∑ i, f (a i) ^ (2 * (m + 1)) := by simp_rw [mul_assoc, mul_sum]; rfl gcongr with a - rw [← div_le_iff'] + rw [← div_le_iff₀'] have := Real.pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) univ m fun i _ ↦ ?_ simpa only [Finset.card_fin, pow_mul] using this all_goals { positivity } diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean index 8ba93a2167..bb1d3b320b 100644 --- a/LeanAPAP/Prereqs/Rudin.lean +++ b/LeanAPAP/Prereqs/Rudin.lean @@ -114,7 +114,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate _ = (2 * exp 2⁻¹) ^ p := by rw [hfp, sq_sqrt, mul_pow, ← exp_nsmul, nsmul_eq_mul, div_eq_mul_inv]; positivity refine le_of_pow_le_pow_left hp₀ (by positivity) ?_ - rwa [hfp, mul_assoc, mul_self_sqrt, mul_pow, ← div_le_iff, ← div_pow] + rwa [hfp, mul_assoc, mul_self_sqrt, mul_pow, ← div_le_iff₀, ← div_pow] all_goals positivity /-- **Rudin's inequality**, usual form. -/ diff --git a/lake-manifest.json b/lake-manifest.json index 9509d9de82..d7e63b603e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0", + "rev": "31fb27d6b89dc94cf7349df247fc44d2a1d130af", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9b07fb6d08b58de5b55813b29f5ac9aa6fa0b1ad", + "rev": "b5f7e1c26c6cb2be97c2ad36bf7038c159e359b3", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,