diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 3b8e5a853f..26cd0fb8cc 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -2,7 +2,7 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField import LeanAPAP.Integer import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar -import LeanAPAP.Mathlib.Data.ENNReal.Basic +import LeanAPAP.Mathlib.Data.Complex.BigOperators import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic import LeanAPAP.Mathlib.Tactic.Positivity @@ -12,7 +12,6 @@ import LeanAPAP.Physics.Unbalancing import LeanAPAP.Prereqs.AddChar.Basic import LeanAPAP.Prereqs.AddChar.MeasurableSpace import LeanAPAP.Prereqs.AddChar.PontryaginDuality -import LeanAPAP.Prereqs.Balance.Complex import LeanAPAP.Prereqs.Bohr.Arc import LeanAPAP.Prereqs.Bohr.Basic import LeanAPAP.Prereqs.Bohr.Regular diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean index b40afd33a8..7e0944f75a 100644 --- a/LeanAPAP/Extras/BSG.lean +++ b/LeanAPAP/Extras/BSG.lean @@ -124,7 +124,7 @@ lemma claim_two : rw [Real.sq_sqrt] exact dconv_nonneg (R := ℝ) indicate_nonneg indicate_nonneg s -- why do I need the annotation?? have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * (A ∩ (s +ᵥ B)).card) - refine div_le_of_nonneg_of_le_mul (by positivity) ?_ ?_ + refine div_le_of_le_mul₀ (by positivity) ?_ ?_ · refine sum_nonneg fun i _ ↦ ?_ -- indicate nonneg should be a positivity lemma exact mul_nonneg (dconv_nonneg indicate_nonneg indicate_nonneg _) (by positivity) diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean index 8fe1efaea8..f88fc34f3b 100644 --- a/LeanAPAP/FiniteField.lean +++ b/LeanAPAP/FiniteField.lean @@ -1,5 +1,5 @@ import Mathlib.FieldTheory.Finite.Basic -import LeanAPAP.Prereqs.Balance.Complex +import LeanAPAP.Mathlib.Data.Complex.BigOperators import LeanAPAP.Prereqs.Chang import LeanAPAP.Prereqs.Convolution.ThreeAP import LeanAPAP.Prereqs.FourierTransform.Convolution @@ -16,7 +16,7 @@ set_option linter.haveLet 0 attribute [-simp] Real.log_inv -open FiniteDimensional Fintype Function MeasureTheory RCLike Real +open Fintype Function MeasureTheory Module RCLike Real open Finset hiding card open scoped ENNReal NNReal BigOperators Combinatorics.Additive Pointwise @@ -28,13 +28,13 @@ local notation "𝓛" x:arg => 1 + log x⁻¹ private lemma one_le_curlog (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 1 ≤ 𝓛 x := by obtain rfl | hx₀ := hx₀.eq_or_lt · simp - have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁ + have : 0 ≤ log x⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 hx₁ linarith private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by obtain rfl | hx₀ := hx₀.eq_or_lt · simp - have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁ + have : 0 ≤ log x⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 hx₁ positivity private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by @@ -42,7 +42,7 @@ private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻ · simp; positivity obtain rfl | hx₁ := hx₁.eq_or_lt · simp - have hx := one_lt_inv hx₀ hx₁ + have hx := (one_lt_inv₀ hx₀).2 hx₁ calc x⁻¹ ^ (𝓛 x)⁻¹ ≤ x⁻¹ ^ (log x⁻¹)⁻¹ := by gcongr @@ -59,11 +59,11 @@ private lemma curlog_mul_le (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) (h calc log x⁻¹ - (x⁻¹ - 1) ≤ 0 := sub_nonpos.2 $ log_le_sub_one_of_pos $ by positivity _ ≤ (x⁻¹ - 1) * log y⁻¹ := - mul_nonneg (sub_nonneg.2 $ one_le_inv hx₀ hx₁) $ log_nonneg $ one_le_inv hy₀ hy₁ + mul_nonneg (sub_nonneg.2 $ (one_le_inv₀ hx₀).2 hx₁) $ log_nonneg $ (one_le_inv₀ hy₀).2 hy₁ private lemma curlog_div_le (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy : 1 ≤ y) : 𝓛 (x / y) ≤ y * 𝓛 x := by - simpa [div_eq_inv_mul] using curlog_mul_le (by positivity) (inv_le_one hy) hx₀ hx₁ + simpa [div_eq_inv_mul] using curlog_mul_le (by positivity) (inv_le_one_of_one_le₀ hy) hx₀ hx₁ private lemma curlog_rpow_le' (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) (hy₁ : y ≤ 1) : 𝓛 (x ^ y) ≤ y⁻¹ * 𝓛 x := by @@ -71,9 +71,10 @@ private lemma curlog_rpow_le' (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) rw [← sub_nonneg] at h ⊢ exact h.trans_eq (by rw [← inv_rpow, log_rpow]; ring; all_goals positivity) calc - 1 - y⁻¹ ≤ 0 := sub_nonpos.2 $ one_le_inv hy₀ hy₁ + 1 - y⁻¹ ≤ 0 := sub_nonpos.2 $ (one_le_inv₀ hy₀).2 hy₁ _ ≤ (y⁻¹ - y) * log x⁻¹ := - mul_nonneg (sub_nonneg.2 $ hy₁.trans $ one_le_inv hy₀ hy₁) $ log_nonneg $ one_le_inv hx₀ hx₁ + mul_nonneg (sub_nonneg.2 $ hy₁.trans $ (one_le_inv₀ hy₀).2 hy₁) $ + log_nonneg $ (one_le_inv₀ hx₀).2 hx₁ private lemma curlog_rpow_le (hx₀ : 0 < x) (hy : 1 ≤ y) : 𝓛 (x ^ y) ≤ y * 𝓛 x := by rw [← inv_rpow, log_rpow, mul_one_add] @@ -91,7 +92,7 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N set p := 2 * ⌈𝓛 γ⌉₊ have hp : 1 < p := Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ.le hγ₁) - have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one $ mod_cast hp + have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one_of_one_lt₀ $ mod_cast hp have hp'' : (p : ℝ≥0).IsConjExponent _ := .conjExponent $ mod_cast hp rw [mul_comm, ← div_div, div_le_iff₀ (zero_lt_two' ℝ)] calc @@ -115,7 +116,7 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N congr any_goals positivity exact ENNReal.natCast_ne_top _ - · have : 1 ≤ γ⁻¹ := one_le_inv hγ hγ₁ + · have : 1 ≤ γ⁻¹ := (one_le_inv₀ hγ).2 hγ₁ have : 0 ≤ log γ⁻¹ := log_nonneg this calc γ ^ (-(↑p)⁻¹ : ℝ) = √(γ⁻¹ ^ ((↑⌈1 + log γ⁻¹⌉₊)⁻¹ : ℝ)) := by @@ -142,8 +143,9 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε have hA₁ : A₁.Nonempty := by simpa using hα₀.trans_le hαA₁ have hA₂ : A₂.Nonempty := by simpa using hα₀.trans_le hαA₂ have hα₁ : α ≤ 1 := hαA₁.trans $ mod_cast A₁.dens_le_one - have : 0 ≤ log α⁻¹ := log_nonneg $ one_le_inv hα₀ hα₁ - have : 0 ≤ log (ε * α)⁻¹ := log_nonneg $ one_le_inv (by positivity) $ mul_le_one hε₁ hα₀.le hα₁ + have : 0 ≤ log α⁻¹ := log_nonneg $ (one_le_inv₀ hα₀).2 hα₁ + have : 0 ≤ log (ε * α)⁻¹ := + log_nonneg $ (one_le_inv₀ (by positivity)).2 $ mul_le_one₀ hε₁ hα₀.le hα₁ obtain rfl | hS := S.eq_empty_or_nonempty · exact ⟨⊤, inferInstance, by simp [hε₀.le]; positivity⟩ have hA₁ : σ[A₁, univ] ≤ α⁻¹ := @@ -156,7 +158,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε ε * α / 4 ≤ ε * 1 / 4 := by gcongr _ ≤ 1 := by linarith obtain ⟨T, hTcard, hTε⟩ := AlmostPeriodicity.linfty_almost_periodicity_boosted ε hε₀ hε₁ k - (by positivity) ((le_inv (by positivity) (by positivity)).2 hα₂) hA₁ univ_nonempty S A₂ hS hA₂ + (by positivity) (le_inv_of_le_inv₀ (by positivity) hα₂) hA₁ univ_nonempty S A₂ hS hA₂ have hT : 0 < (T.card : ℝ) := hTcard.trans_lt' (by positivity) replace hT : T.Nonempty := by simpa using hT let Δ := largeSpec (μ T) 2⁻¹ @@ -186,7 +188,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog (by positivity) sorry _ ≤ 2 * (4 * 𝓛 (ε * α)) := by gcongr - exact curlog_div_le (by positivity) (mul_le_one hε₁ hα₀.le hα₁) (by norm_num) + exact curlog_div_le (by positivity) (mul_le_one₀ hε₁ hα₀.le hα₁) (by norm_num) _ = 2 ^ 3 * 𝓛 (ε * α) := by ring _ = 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring_nf calc @@ -250,7 +252,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) ∃ p' : ℕ, p' ≤ 2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p ∧ 1 + ε / 2 / 2 ≤ ‖card G • (f ○ f) + 1‖_[p', μ univ] := by refine unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ.le hγ₁).ne') - (ε / 2) (by positivity) (div_le_one_of_le (hε₁.le.trans $ by norm_num) $ by norm_num) + (ε / 2) (by positivity) (div_le_one_of_le₀ (hε₁.le.trans $ by norm_num) $ by norm_num) (card G • (balance (μ A) ○ balance (μ A))) (sqrt (card G) • balance (μ A)) (μ univ) ?_ ?_ ?_ · ext a : 1 simp [smul_dconv, dconv_smul, smul_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow] @@ -268,7 +270,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) have : 0 < log (64 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith) have : 1 ≤ 𝓛 γ := one_le_curlog hγ.le hγ₁ have : 0 < q' := by positivity - have : 1 ≤ ε⁻¹ := one_le_inv hε₀ hε₁.le + have : 1 ≤ ε⁻¹ := (one_le_inv₀ hε₀).2 hε₁.le have := calc (q' : ℝ) ≤ ↑(2 * ⌈2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p + 2 ^ 8 * ε⁻¹ ^ 2 * (64 / ε)⌉₊) := by @@ -288,7 +290,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) (2⁻¹ : ℝ) ≤ 2 ^ 15 * 1 * 1 := by norm_num _ ≤ 2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ := ?_ gcongr - exact one_le_pow₀ (one_le_inv hε₀ hε₁.le) + exact one_le_pow₀ ((one_le_inv₀ hε₀).2 hε₁.le) _ = 2 ^ 17 * 𝓛 γ / ε ^ 3 := by ring obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G), 1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ μ A₂) x ∧ @@ -301,7 +303,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) gcongr · norm_num · norm_num - · exact one_le_inv hε₀ hε₁.le + · exact (one_le_inv₀ hε₀).2 hε₁.le · norm_num _ ≤ ⌈2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ := Nat.le_ceil _ _ = ↑(1 * ⌈0 + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊) := by rw [one_mul, zero_add] @@ -362,12 +364,12 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) _ ≤ 2 ^ 32 * (8 * q' * 𝓛 α) ^ 2 * (2 ^ 8 * q' * 𝓛 α / ε) ^ 2 * (ε / 32)⁻¹ ^ 2 := by have : α ^ (2 * q') ≤ 1 := pow_le_one₀ hα₀.le hα₁ - have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one (by norm_num) (by positivity) ‹_› - have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one (by linarith) (by positivity) ‹_› + have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one₀ (by norm_num) (by positivity) ‹_› + have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one₀ (by linarith) (by positivity) ‹_› have : 0 ≤ log (ε / 32 * (4⁻¹ * α ^ (2 * q')))⁻¹ := - log_nonneg $ one_le_inv (by positivity) ‹_› - have : 0 ≤ log (4⁻¹ * α ^ (2 * q'))⁻¹ := log_nonneg $ one_le_inv (by positivity) ‹_› - have : 0 ≤ log (α ^ (2 * q'))⁻¹ := log_nonneg $ one_le_inv (by positivity) ‹_› + log_nonneg $ (one_le_inv₀ (by positivity)).2 ‹_› + have : 0 ≤ log (4⁻¹ * α ^ (2 * q'))⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 ‹_› + have : 0 ≤ log (α ^ (2 * q'))⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 ‹_› have := calc 𝓛 (4⁻¹ * α ^ (2 * q')) ≤ 4⁻¹⁻¹ * 𝓛 (α ^ (2 * q')) := @@ -434,7 +436,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr have : NeZero q := ⟨by positivity⟩ have : Fact q.Prime := ⟨hq⟩ have hq' : Odd q := hq.odd_of_ne_two $ by rintro rfl; simp at hq₃ - have : 1 ≤ α⁻¹ := one_le_inv (by positivity) (by simp [α]) + have : 1 ≤ α⁻¹ := (one_le_inv₀ (by positivity)).2 (by simp [α]) have hα₀ : 0 < α := by positivity have : 0 ≤ log α⁻¹ := log_nonneg ‹_› have : 0 < 𝓛 α := by positivity @@ -525,13 +527,13 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr calc _ ≤ (1 : ℝ) := mod_cast dens_le_one _ < _ := ?_ - rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff₀] + rw [← inv_lt_iff_one_lt_mul₀, lt_pow_iff_log_lt, ← div_lt_iff₀] calc log α⁻¹ / log (65 / 64) < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _ _ = ⌊(log (65 / 64) + log α⁻¹) / log (65 / 64)⌋₊ := by rw [add_comm (log _), ← 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 + exact div_nonneg (log_nonneg $ (one_le_inv₀ (by positivity)).2 (by simp [α])) aux.le _ ≤ ⌊𝓛 α / log (65 / 64)⌋₊ := by gcongr calc @@ -555,7 +557,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr _ = 2 ^ 148 * (log (65 / 64)) ⁻¹ * 𝓛 α ^ 9 := by ring _ ≤ 2 ^ 148 * 2 ^ 7 * 𝓛 α ^ 9 := by gcongr - rw [inv_le ‹_› (by positivity)] + refine inv_le_of_inv_le₀ (by positivity) ?_ calc (2 ^ 7)⁻¹ ≤ 1 - (65 / 64)⁻¹ := by norm_num _ ≤ log (65 / 64) := one_sub_inv_le_log_of_pos (by positivity) diff --git a/LeanAPAP/Mathlib/Data/Complex/BigOperators.lean b/LeanAPAP/Mathlib/Data/Complex/BigOperators.lean new file mode 100644 index 0000000000..f10c287db8 --- /dev/null +++ b/LeanAPAP/Mathlib/Data/Complex/BigOperators.lean @@ -0,0 +1,11 @@ +import Mathlib.Data.Complex.BigOperators + +open Fintype + +namespace Complex +variable {ι : Type*} + +@[simp] lemma ofReal'_comp_balance [Fintype ι] (f : ι → ℝ) : + ofReal' ∘ balance f = balance (ofReal' ∘ f) := ofReal_comp_balance _ + +end Complex diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean b/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean deleted file mode 100644 index 4b0c8e2c35..0000000000 --- a/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean +++ /dev/null @@ -1,32 +0,0 @@ -import Mathlib.Data.ENNReal.Basic - -namespace ENNReal - -@[simp] lemma ofNat_pos {n : ℕ} [n.AtLeastTwo] : 0 < (no_index OfNat.ofNat n : ℝ≥0∞) := - Nat.cast_pos.2 Fin.size_pos' - -end ENNReal - -namespace Mathlib.Meta.Positivity -open Lean Meta Qq Function ENNReal - -private lemma ennreal_one_pos : (0 : ℝ≥0∞) < 1 := zero_lt_one - -/-- The `positivity` extension which identifies expressions of the form `‖f‖_[p]`. -/ -@[positivity OfNat.ofNat _] def evalOfNatENNReal : PositivityExt where eval {u} α _z _p e := do - match u, α, e with - | 0, ~q(ℝ≥0∞), ~q(@OfNat.ofNat _ $n $instn) => - try - let instn ← synthInstanceQ q(Nat.AtLeastTwo $n) - return Strictness.positive (q(@ofNat_pos $n $instn) : Expr) - catch _ => do - match n with - | ~q(1) => return .positive (q(ennreal_one_pos) : Expr) - | _ => throwError "not positive" - | _ => throwError "not `ENNReal`-valued `ofNat`" - -end Mathlib.Meta.Positivity - -open scoped ENNReal - -example : (0 : ℝ≥0∞) < 1 := by positivity diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean index 2a8335967c..c831c2906c 100644 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean +++ b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean @@ -7,31 +7,7 @@ open scoped ENNReal variable {α β : Type*} {m : MeasurableSpace α} [ConditionallyCompleteLattice β] {μ : Measure α} {f : α → β} -section SMul -variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] - [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞} - --- TODO: Replace in mathlib -@[simp] lemma essSup_smul_measure' {f : α → β} {c : ℝ≥0∞} (hc : c ≠ 0) : - essSup f (c • μ) = essSup f μ := by simp_rw [essSup, Measure.ae_smul_measure_eq hc] - -end SMul - -variable [Nonempty α] - -lemma essSup_eq_ciSup (hμ : ∀ a, μ {a} ≠ 0) (hf : BddAbove (Set.range f)) : - essSup f μ = ⨆ a, f a := by rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf] - -lemma essInf_eq_ciInf (hμ : ∀ a, μ {a} ≠ 0) (hf : BddBelow (Set.range f)) : - essInf f μ = ⨅ a, f a := by rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf] - -variable [MeasurableSingletonClass α] - -@[simp] lemma essSup_count_eq_ciSup (hf : BddAbove (Set.range f)) : - essSup f .count = ⨆ a, f a := essSup_eq_ciSup (by simp) hf - -@[simp] lemma essInf_count_eq_ciInf (hf : BddBelow (Set.range f)) : - essInf f .count = ⨅ a, f a := essInf_eq_ciInf (by simp) hf +variable [Nonempty α] [MeasurableSingletonClass α] @[simp] lemma essSup_cond_count_eq_ciSup [Finite α] (hf : BddAbove (Set.range f)) : essSup f .count[|.univ] = ⨆ a, f a := essSup_eq_ciSup (by simp [cond_apply, Set.finite_univ]) hf diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index f79d543bad..8aac4a5e15 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -91,7 +91,7 @@ variable {G : Type*} [Fintype G] {A S : Finset G} {f : G → ℂ} {x ε K : ℝ} local notation "𝓛" x => 1 + log (min 1 x)⁻¹ private lemma curlog_pos (hx₀ : 0 < x) : 0 < 𝓛 x := by - have : 0 ≤ log (min 1 x)⁻¹ := log_nonneg $ one_le_inv (by positivity) inf_le_left + have : 0 ≤ log (min 1 x)⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 inf_le_left positivity section @@ -433,7 +433,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ have hm₀ : 0 < m := curlog_pos (by positivity) have hm₁ : 1 ≤ ⌈m⌉₊ := Nat.one_le_iff_ne_zero.2 $ by positivity obtain ⟨T, hKT, hT⟩ := almost_periodicity (ε / exp 1) (by positivity) - (div_le_one_of_le (hε₁.trans $ one_le_exp zero_le_one) $ by positivity) ⌈m⌉₊ (𝟭 B) hK₂ hK + (div_le_one_of_le₀ (hε₁.trans $ one_le_exp zero_le_one) $ by positivity) ⌈m⌉₊ (𝟭 B) hK₂ hK norm_cast at hT set M : ℕ := 2 * ⌈m⌉₊ have hM₀ : (M : ℝ≥0) ≠ 0 := by positivity @@ -481,13 +481,13 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ ≤ r ^ (-(M : ℝ)⁻¹) := rpow_le_rpow_of_nonpos (by positivity) inf_le_right $ neg_nonpos.2 $ by positivity _ ≤ r ^ (-(1 + log r⁻¹)⁻¹) := - rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left $ neg_le_neg $ inv_le_inv_of_le + rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left $ neg_le_neg $ inv_anti₀ (by positivity) $ (Nat.le_ceil _).trans $ mod_cast Nat.le_mul_of_pos_left _ (by positivity) _ ≤ r ^ (-(0 + log r⁻¹)⁻¹) := by obtain hr | hr : r = 1 ∨ r < 1 := inf_le_left.eq_or_lt · simp [hr] - have : 0 < log r⁻¹ := log_pos <| one_lt_inv (by positivity) hr + have : 0 < log r⁻¹ := log_pos <| (one_lt_inv₀ (by positivity)).2 hr exact rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left (by gcongr; exact zero_le_one) _ = r ^ (log r)⁻¹ := by simp [inv_neg] _ ≤ exp 1 := rpow_inv_log_le_exp_one @@ -499,7 +499,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : K ^ (-4096 * ⌈𝓛 (C.card / B.card)⌉ * k ^ 2/ ε ^ 2) * S.card ≤ T.card ∧ ‖μ T ∗^ k ∗ (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by obtain ⟨T, hKT, hT⟩ := linfty_almost_periodicity (ε / k) (by positivity) - (div_le_one_of_le (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK + (div_le_one_of_le₀ (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK _ _ hB hC refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩ set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 4887087d8a..f8f5f8e873 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -126,7 +126,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ mul_div_right_comm] using h positivity refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right - ?_ $ div_le_one_of_le ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le ?_ ?_⟩ + ?_ $ div_le_one_of_le₀ ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le₀ ?_ ?_⟩ · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, ← Nat.cast_smul_eq_nsmul ℝ, wInner_smul_left, star_trivial, mul_assoc] any_goals positivity @@ -223,7 +223,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 := ?_ _ ≤ _ := mul_le_of_le_one_left (mul_nonneg (hp.pow_nonneg _) $ hp.pow_nonneg _) $ - mul_le_one dL1Norm_mu_le_one (NNReal.coe_nonneg _) dL1Norm_mu_le_one + mul_le_one₀ dL1Norm_mu_le_one (NNReal.coe_nonneg _) dL1Norm_mu_le_one _ ≤ _ := mul_le_mul_of_nonneg_right ?_ $ hp.pow_nonneg _ · have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ := dconv_nonneg mu_nonneg mu_nonneg simp_rw [← NNReal.coe_mul, ← dL1Norm_dconv mu_nonneg mu_nonneg, dL1Norm_eq_sum_nnnorm, diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index adf5dda556..0c19f96169 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -219,13 +219,13 @@ lemma unbalancing' (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁ (2⁻¹ : ℝ) ≤ 120 * 1 * 1 * 1 := by norm_num _ ≤ 120 * ε⁻¹ * log (3 * ε⁻¹) * p := by gcongr - · exact one_le_inv hε₀ hε₁ + · exact (one_le_inv₀ hε₀).2 hε₁ · rw [← log_exp 1] gcongr calc exp 1 ≤ 2.7182818286 := exp_one_lt_d9.le _ ≤ 3 * 1 := by norm_num - _ ≤ 3 * ε⁻¹ := by gcongr; exact one_le_inv hε₀ hε₁ + _ ≤ 3 * ε⁻¹ := by gcongr; exact (one_le_inv₀ hε₀).2 hε₁ · exact mod_cast hp _ ≤ 2 * (120 * ε⁻¹ * (3 * ε⁻¹) * p) := by gcongr; exact Real.log_le_self (by positivity) _ ≤ 2 * (2 ^ 7 * ε⁻¹ * (2 ^ 2 * ε⁻¹) * p) := by gcongr <;> norm_num diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean index 37d7ec69aa..26d923981c 100644 --- a/LeanAPAP/Prereqs/AddChar/Basic.lean +++ b/LeanAPAP/Prereqs/AddChar/Basic.lean @@ -71,7 +71,7 @@ noncomputable instance instFintype [Finite G] : Fintype (AddChar G R) := @Fintype.ofFinite _ (AddChar.linearIndependent G R).finite @[simp] lemma card_addChar_le [Fintype G] : card (AddChar G R) ≤ card G := by - simpa only [FiniteDimensional.finrank_fintype_fun_eq_card] using + simpa only [Module.finrank_fintype_fun_eq_card] using (AddChar.linearIndependent G R).fintype_card_le_finrank end RCLike diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean index 4a7f2b6b28..e22240be06 100644 --- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean +++ b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean @@ -142,7 +142,7 @@ variable (α) [Finite α] /-- Complex-valued characters of a finite abelian group `α` form a basis of `α → ℂ`. -/ def complexBasis : Basis (AddChar α ℂ) ℂ (α → ℂ) := basisOfLinearIndependentOfCardEqFinrank (AddChar.linearIndependent _ _) $ by - cases nonempty_fintype α; rw [card_eq, FiniteDimensional.finrank_fintype_fun_eq_card] + cases nonempty_fintype α; rw [card_eq, Module.finrank_fintype_fun_eq_card] @[simp, norm_cast] lemma coe_complexBasis : ⇑(complexBasis α) = ((⇑) : AddChar α ℂ → α → ℂ) := by diff --git a/LeanAPAP/Prereqs/Balance/Complex.lean b/LeanAPAP/Prereqs/Balance/Complex.lean deleted file mode 100644 index e811bde46c..0000000000 --- a/LeanAPAP/Prereqs/Balance/Complex.lean +++ /dev/null @@ -1,31 +0,0 @@ -import Mathlib.Algebra.BigOperators.Balance -import Mathlib.Analysis.RCLike.Basic -import Mathlib.Data.Complex.BigOperators - -open Fintype -open scoped NNReal - -namespace Complex -variable {ι : Type*} - -@[simp] lemma ofReal_comp_balance [Fintype ι] (f : ι → ℝ) : - ofReal ∘ balance f = balance (ofReal ∘ f) := by simp [balance] - -@[simp] lemma ofReal'_comp_balance [Fintype ι] (f : ι → ℝ) : - ofReal' ∘ balance f = balance (ofReal' ∘ f) := ofReal_comp_balance _ - -end Complex - -namespace RCLike -variable {ι 𝕜 : Type*} [RCLike 𝕜] [Fintype ι] (f : ι → ℝ) (a : ι) - -@[simp, norm_cast] -lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_balance (algebraMap ..) .. - -@[simp] lemma coe_comp_balance : ((↑) : ℝ → 𝕜) ∘ balance f = balance ((↑) ∘ f) := - funext $ coe_balance _ - -@[simp] lemma ofReal_comp_balance : ofReal ∘ balance f = balance (ofReal ∘ f : ι → 𝕜) := by - simp [balance] - -end RCLike diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index 744df2bd23..31f47c7b37 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -1,6 +1,5 @@ import Mathlib.Algebra.Order.Chebyshev import Mathlib.Analysis.MeanInequalities -import LeanAPAP.Mathlib.Data.ENNReal.Basic import LeanAPAP.Prereqs.Energy import LeanAPAP.Prereqs.LargeSpec import LeanAPAP.Prereqs.Rudin @@ -20,7 +19,7 @@ local notation "𝓛" x:arg => 1 + log x⁻¹ private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by obtain rfl | hx₀ := hx₀.eq_or_lt · simp - have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁ + have : 0 ≤ log x⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 hx₁ positivity private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by @@ -28,7 +27,7 @@ private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻ · simp; positivity obtain rfl | hx₁ := hx₁.eq_or_lt · simp - have hx := one_lt_inv hx₀ hx₁ + have hx := (one_lt_inv₀ hx₀).2 hx₁ calc x⁻¹ ^ (𝓛 x)⁻¹ ≤ x⁻¹ ^ (log x⁻¹)⁻¹ := by gcongr @@ -80,7 +79,7 @@ local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s variable [MeasurableSpace G] [DiscreteMeasurableSpace G] private lemma α_le_one (f : G → ℂ) : ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G ≤ 1 := by - refine div_le_one_of_le (div_le_of_nonneg_of_le_mul ?_ ?_ ?_) ?_ + refine div_le_one_of_le₀ (div_le_of_le_mul₀ ?_ ?_ ?_) ?_ any_goals positivity rw [dL1Norm_eq_sum_nnnorm, dL2Norm_sq_eq_sum_nnnorm, ← NNReal.coe_le_coe] push_cast @@ -190,7 +189,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) : rw [div_self hη.ne', one_pow, one_mul] _ = _ := by ring refine le_mul_of_one_le_right (by positivity) ?_ - rw [← inv_pos_le_iff_one_le_mul'] + rw [← inv_le_iff_one_le_mul₀'] calc α⁻¹ = exp (0 + log α⁻¹) := by rw [zero_add, exp_log]; norm_cast; positivity _ ≤ exp ⌈0 + log α⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _ diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean index 42a2190810..add9415fcd 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean @@ -1,11 +1,8 @@ -import Mathlib.Algebra.Order.BigOperators.Expect import Mathlib.Algebra.Star.Conjneg -import Mathlib.Data.Finset.Density import Mathlib.Data.Fintype.Order -import Mathlib.Probability.ConditionalProbability import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup -import LeanAPAP.Prereqs.Function.Translate import LeanAPAP.Prereqs.Function.Indicator.Defs +import LeanAPAP.Prereqs.Function.Translate import LeanAPAP.Prereqs.NNLpNorm /-! diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean index f21a8e6a60..405c8fc81e 100644 --- a/LeanAPAP/Prereqs/Rudin.lean +++ b/LeanAPAP/Prereqs/Rudin.lean @@ -1,6 +1,5 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series -import LeanAPAP.Mathlib.Data.ENNReal.Basic import LeanAPAP.Prereqs.FourierTransform.Compact import LeanAPAP.Prereqs.Randomisation @@ -83,7 +82,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate _ ≤ 𝔼 a, |(f a).re| ^ p / p ! := by gcongr; norm_cast; exact p.factorial_le_pow _ ≤ 𝔼 a, exp |(f a).re| := by gcongr; exact pow_div_factorial_le_exp _ (abs_nonneg _) _ _ ≤ _ := rudin_exp_abs_ineq f hf - _ ≤ 2 ^ p * exp (‖f‖ₙ_[2] ^ 2 / 2) := by gcongr; exact le_self_pow one_le_two hp₀ + _ ≤ 2 ^ p * exp (‖f‖ₙ_[2] ^ 2 / 2) := by gcongr; exact le_self_pow₀ one_le_two hp₀ _ = (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) ?_ diff --git a/lake-manifest.json b/lake-manifest.json index d5319ed35d..0845906a16 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f274aed7ae8d1addd3e70adaf3183ccc6e1ed43d", + "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", + "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad", + "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -44,7 +44,7 @@ {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "", + "scope": "leanprover", "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1", + "rev": "7376ac07aa2b0492372c056b7a2c3163b3026d1e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "781beceb959c68b36d3d96205b3531e341879d2c", + "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d369bba55fcefeb0d7600e9c2e4856ac9bbece72", + "rev": "e4fa33c4f2bc49e66f5d06e91e21fe2279ad7e14", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 89985206ac..eff86fd63d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0 +leanprover/lean4:v4.13.0-rc3