From 56b5b35aa11a356d980ec1f2134643789da00fcb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 29 Jul 2024 20:33:17 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 11 ++++- LeanAPAP/Mathlib/Algebra/Algebra/Basic.lean | 19 ++++----- .../BigOperators/{Pi.lean => Ring.lean} | 2 - .../Mathlib/Data/Fintype/BigOperators.lean | 15 +++++++ LeanAPAP/Mathlib/Data/Fintype/Pi.lean | 19 --------- LeanAPAP/Physics/AlmostPeriodicity.lean | 14 ++++--- LeanAPAP/Prereqs/Chang.lean | 4 +- .../Prereqs/Convolution/Discrete/Basic.lean | 7 ++-- LeanAPAP/Prereqs/Expect/Basic.lean | 14 ++++--- LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Weighted.lean | 2 +- LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 24 ++++++----- LeanAPAP/Prereqs/Multinomial.lean | 41 +------------------ lake-manifest.json | 10 ++--- 14 files changed, 77 insertions(+), 107 deletions(-) rename LeanAPAP/Mathlib/Algebra/BigOperators/{Pi.lean => Ring.lean} (96%) create mode 100644 LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean delete mode 100644 LeanAPAP/Mathlib/Data/Fintype/Pi.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index fa66fca114..8ba9332da9 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -1,14 +1,20 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField.Basic import LeanAPAP.Mathlib.Algebra.Algebra.Basic -import LeanAPAP.Mathlib.Algebra.BigOperators.Pi +import LeanAPAP.Mathlib.Algebra.BigOperators.Ring import LeanAPAP.Mathlib.Algebra.Group.AddChar import LeanAPAP.Mathlib.Algebra.Order.Module.Defs import LeanAPAP.Mathlib.Analysis.Complex.Circle import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle -import LeanAPAP.Mathlib.Data.Fintype.Pi +import LeanAPAP.Mathlib.Data.Fintype.BigOperators import LeanAPAP.Mathlib.Data.Rat.Cast.Defs import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas +import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup +import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic +import LeanAPAP.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic +import LeanAPAP.Mathlib.MeasureTheory.Measure.Count +import LeanAPAP.Mathlib.MeasureTheory.OuterMeasure.AE +import LeanAPAP.Mathlib.Order.LiminfLimsup import LeanAPAP.Mathlib.Tactic.Positivity import LeanAPAP.Physics.AlmostPeriodicity import LeanAPAP.Physics.DRC @@ -28,6 +34,7 @@ import LeanAPAP.Prereqs.Convolution.ThreeAP import LeanAPAP.Prereqs.Convolution.WithConv import LeanAPAP.Prereqs.Curlog import LeanAPAP.Prereqs.Energy +import LeanAPAP.Prereqs.EssSupCount import LeanAPAP.Prereqs.Expect.Basic import LeanAPAP.Prereqs.Expect.Complex import LeanAPAP.Prereqs.FourierTransform.Compact diff --git a/LeanAPAP/Mathlib/Algebra/Algebra/Basic.lean b/LeanAPAP/Mathlib/Algebra/Algebra/Basic.lean index 1094cb565b..195ffe931c 100644 --- a/LeanAPAP/Mathlib/Algebra/Algebra/Basic.lean +++ b/LeanAPAP/Mathlib/Algebra/Algebra/Basic.lean @@ -1,19 +1,18 @@ import Mathlib.Algebra.Algebra.Basic import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas -open NNRat - variable {F α β : Type*} +namespace NNRat section DivisionSemiring variable [DivisionSemiring α] [CharZero α] [DivisionSemiring β] [CharZero β] -instance NNRat.instAlgebra : Algebra ℚ≥0 α where +instance instAlgebra : Algebra ℚ≥0 α where smul_def' := smul_def toRingHom := castHom α commutes' := cast_commute -instance NNRat.instlinearMapClass [FunLike F α β] [RingHomClass F α β] : +instance instlinearMapClass [FunLike F α β] [RingHomClass F α β] : LinearMapClass F ℚ≥0 α β where map_smulₛₗ f q a := by simp [smul_def, cast_id] @@ -22,10 +21,10 @@ end DivisionSemiring section Semifield variable [Semifield β] [CharZero β] [SMul α β] -instance NNRat.instSMulCommClass [SMulCommClass α β β] : SMulCommClass ℚ≥0 α β where +instance instSMulCommClass [SMulCommClass α β β] : SMulCommClass ℚ≥0 α β where smul_comm q a b := by simp [smul_def, mul_smul_comm] -instance NNRat.instSMulCommClass' [SMulCommClass β α β] : SMulCommClass α ℚ≥0 β := +instance instSMulCommClass' [SMulCommClass β α β] : SMulCommClass α ℚ≥0 β := have := SMulCommClass.symm β α β SMulCommClass.symm _ _ _ @@ -35,13 +34,13 @@ section Semifield variable [Semifield α] [CharZero α] [Semiring β] [CharZero β] [NNRatCast β] [Module ℚ≥0 β] variable (α) in --- TODO: Change `nnsmul_eq_smul_cast` to match /-- `nnqsmul` is equal to any other module structure via a cast. -/ -lemma _root_.nnratCast_smul_eq_nnqsmul [Module α β] (q : ℚ≥0) (a : β) : (q : α) • a = q • a := by +lemma cast_smul_eq_nnqsmul [Module α β] (q : ℚ≥0) (a : β) : (q : α) • a = q • a := by refine MulAction.injective₀ (α := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_ dsimp - rw [← mul_smul, den_mul_eq_num, ← nsmul_eq_smul_cast, ← nsmul_eq_smul_cast, ← smul_assoc, + rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, ← smul_assoc, nsmul_eq_mul q.den, ← cast_natCast, ←cast_mul, den_mul_eq_num, cast_natCast, - ← nsmul_eq_smul_cast] + Nat.cast_smul_eq_nsmul] end Semifield +end NNRat diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean similarity index 96% rename from LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean rename to LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean index 542b7642a0..fafd3b8057 100644 --- a/LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean +++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean @@ -1,6 +1,4 @@ -import Mathlib.Algebra.BigOperators.Pi import Mathlib.Algebra.BigOperators.Ring -import LeanAPAP.Mathlib.Data.Fintype.Pi open Finset diff --git a/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean b/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean new file mode 100644 index 0000000000..942ac5d1ce --- /dev/null +++ b/LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean @@ -0,0 +1,15 @@ +import Mathlib.Data.Fintype.BigOperators + +open Finset + +namespace Fintype +variable {α β : Type*} {δ : α → Type*} {s : Finset α} {n : ℕ} + +local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s + +protected lemma _root_.Finset.Nonempty.piFinset_const (hs : s.Nonempty) : (s ^^ n).Nonempty := + piFinset_nonempty.2 fun _ ↦ hs + +lemma card_piFinset_const (s : Finset α) (n : ℕ) : (s ^^ n).card = s.card ^ n := by simp + +end Fintype diff --git a/LeanAPAP/Mathlib/Data/Fintype/Pi.lean b/LeanAPAP/Mathlib/Data/Fintype/Pi.lean deleted file mode 100644 index 22dcc9986a..0000000000 --- a/LeanAPAP/Mathlib/Data/Fintype/Pi.lean +++ /dev/null @@ -1,19 +0,0 @@ -import Mathlib.Data.Fintype.BigOperators - -open Finset - -namespace Fintype -variable {α β : Type*} {δ : α → Type*} {s : Finset α} {n : ℕ} - -@[reducible] -def piFinsetConst (s : Finset α) (n : ℕ) := piFinset fun _ : Fin n ↦ s - -infixl:70 "^^" => piFinsetConst - -protected lemma _root_.Finset.Nonempty.piFinsetConst (hs : s.Nonempty) : (s ^^ n).Nonempty := - piFinset_nonempty.2 fun _ ↦ hs - -@[simp] lemma card_piFinsetConst (s : Finset α) (n : ℕ) : (s ^^ n).card = s.card ^ n := by - simp [piFinsetConst, card_piFinset] - -end Fintype diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index 4e6cedf1cb..4c76c70a09 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -87,6 +87,8 @@ variable {G : Type*} [DecidableEq G] [Fintype G] [AddCommGroup G] {A S : Finset open Finset Real open scoped BigOperators Pointwise NNReal ENNReal +local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s + namespace AlmostPeriodicity def LProp (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) (a : Fin k → G) : Prop := @@ -102,10 +104,10 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m) ‖fun x : G ↦ ∑ i : Fin k, f (x - a i) - (k • (mu A ∗ f)) x‖_[2 * m] ^ (2 * m) ≤ 1 / 2 * (k * ε * ‖f‖_[2 * m]) ^ (2 * m) * A.card ^ k) : (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by - rw [←Nat.cast_pow, ←Fintype.card_piFinsetConst] at h + rw [←Nat.cast_pow, ←Fintype.card_piFinset_const] at h have := my_other_markov (by positivity) (by norm_num) (fun _ _ ↦ by positivity) h norm_num1 at this - rw [Fintype.card_piFinsetConst, mul_comm, mul_one_div, Nat.cast_pow] at this + rw [Fintype.card_piFinset_const, mul_comm, mul_one_div, Nat.cast_pow] at this refine this.trans_eq ?_ rw [l] congr with a : 3 @@ -212,7 +214,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := lemma28_part_two hm hA refine this.trans ?_ - simp only [sum_const, Fintype.card_piFinsetConst, nsmul_eq_mul, Nat.cast_pow] + simp only [sum_const, Fintype.card_piFinset_const, nsmul_eq_mul, Nat.cast_pow] refine (lemma28_end hε hm hk).trans_eq' ?_ simp only [mul_assoc, card_fin] @@ -304,7 +306,7 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0) have hS' : 0 < S.card := by rwa [card_pos] have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by refine (card_le_card (add_subset_add_right hL)).trans ?_ - rw [←Fintype.card_piFinsetConst] + rw [←Fintype.card_piFinset_const] refine card_le_card fun i hi ↦ ?_ simp only [mem_add, mem_piDiag, Fintype.mem_piFinset, exists_prop, exists_and_left, exists_exists_and_eq_and] at hi ⊢ @@ -482,10 +484,10 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : calc ‖μ T ∗^ k ∗ F - F‖_[∞] = ‖𝔼 a ∈ T ^^ k, (τ (∑ i, a i) F - F)‖_[∞] := by - rw [mu_iterConv_conv, expect_sub_distrib, expect_const hT'.piFinsetConst] + rw [mu_iterConv_conv, expect_sub_distrib, expect_const hT'.piFinset_const] _ ≤ 𝔼 a ∈ T ^^ k, ‖τ (∑ i, a i) F - F‖_[∞] := lpNorm_expect_le le_top _ _ _ ≤ 𝔼 _a ∈ T ^^ k, ε := expect_le_expect fun x hx ↦ ?_ - _ = ε := by rw [expect_const hT'.piFinsetConst] + _ = ε := by rw [expect_const hT'.piFinset_const] calc ‖τ (∑ i, x i) F - F‖_[⊤] _ ≤ ∑ i, ‖τ (x i) F - F‖_[⊤] := lpNorm_translate_sum_sub_le le_top _ _ _ diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index b5191cded3..f2ecf4ec09 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -12,9 +12,11 @@ import LeanAPAP.Prereqs.Rudin open Finset Fintype Function Real open scoped ComplexConjugate ComplexOrder NNReal -variable {G : Type*} [AddCommGroup G] [Fintype G] {f : G → ℂ} {η : ℝ} {ψ : AddChar G ℂ} + variable {G : Type*} [AddCommGroup G] [Fintype G] {f : G → ℂ} {η : ℝ} {ψ : AddChar G ℂ} {Δ : Finset (AddChar G ℂ)} {m : ℕ} +local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s + private noncomputable def α (f : G → ℂ) := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G lemma α_nonneg (f : G → ℂ) : 0 ≤ α f := by unfold α; positivity diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean index 95fef2c630..a675bed3f5 100644 --- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean +++ b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean @@ -1,6 +1,5 @@ import Mathlib.Algebra.Module.Pi import Mathlib.Analysis.Complex.Basic -import LeanAPAP.Mathlib.Data.Fintype.Pi import LeanAPAP.Prereqs.Function.Indicator.Basic import LeanAPAP.Prereqs.Convolution.Discrete.Defs @@ -34,6 +33,8 @@ point in time. Multiplicativise? Probably ugly and not very useful. -/ +local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s + open Finset Fintype Function open scoped BigOperators ComplexConjugate NNReal Pointwise @@ -166,8 +167,8 @@ variable [Semifield β] [CharZero β] [Module ℚ≥0 β] [StarRing β] lemma mu_iterConv_conv (s : Finset α) (n : ℕ) (f : α → β) : μ s ∗^ n ∗ f = 𝔼 a ∈ piFinset (fun _ : Fin n ↦ s), τ (∑ i, a i) f := by simp only [mu, smul_iterConv, inv_pow, smul_conv, indicate_iterConv_conv, expect, - card_piFinsetConst, Nat.cast_pow] - rw [← nnratCast_smul_eq_nnqsmul β] + card_piFinset_const, Nat.cast_pow] + rw [← NNRat.cast_smul_eq_nnqsmul β] push_cast rfl diff --git a/LeanAPAP/Prereqs/Expect/Basic.lean b/LeanAPAP/Prereqs/Expect/Basic.lean index ee17eb4421..59ee4dc323 100644 --- a/LeanAPAP/Prereqs/Expect/Basic.lean +++ b/LeanAPAP/Prereqs/Expect/Basic.lean @@ -3,7 +3,7 @@ import Mathlib.Analysis.RCLike.Basic import Mathlib.Tactic.Positivity.Finset import LeanAPAP.Mathlib.Algebra.Algebra.Basic import LeanAPAP.Mathlib.Algebra.Order.Module.Defs -import LeanAPAP.Mathlib.Data.Fintype.Pi +import LeanAPAP.Mathlib.Data.Fintype.BigOperators /-! # Average over a finset @@ -215,14 +215,14 @@ lemma _root_.map_expect {F : Type*} [FunLike F α β] [LinearMapClass F ℚ≥0 lemma card_smul_expect (s : Finset ι) (f : ι → α) : s.card • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by obtain rfl | hs := s.eq_empty_or_nonempty · simp - · rw [expect, nsmul_eq_smul_cast ℚ≥0, smul_inv_smul₀] + · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀] positivity @[simp] nonrec lemma _root_.Fintype.card_smul_expect [Fintype ι] (f : ι → α) : Fintype.card ι • 𝔼 i, f i = ∑ i, f i := card_smul_expect _ _ @[simp] lemma expect_const (hs : s.Nonempty) (a : α) : 𝔼 _i ∈ s, a = a := by - rw [expect, sum_const, nsmul_eq_smul_cast ℚ≥0, inv_smul_smul₀]; positivity + rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]; positivity lemma smul_expect {G : Type*} [DistribSMul G α] [SMulCommClass G ℚ≥0 α] (a : G) (s : Finset ι) (f : ι → α) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by @@ -297,10 +297,12 @@ end Semiring section CommSemiring variable [CommSemiring α] [Module ℚ≥0 α] [IsScalarTower ℚ≥0 α α] [SMulCommClass ℚ≥0 α α] +local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s + lemma expect_pow (s : Finset ι) (f : ι → α) (n : ℕ) : (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ s ^^ n, ∏ i, f (p i) := by classical - rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinsetConst, inv_pow, Nat.cast_pow] + rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow] end CommSemiring @@ -358,11 +360,11 @@ lemma _root_.GCongr.expect_le_expect (h : ∀ i ∈ s, f i ≤ g i) : s.expect f lemma expect_le (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, f x ≤ a) : 𝔼 i ∈ s, f i ≤ a := (inv_smul_le_iff_of_pos $ by positivity).2 $ by - rw [←nsmul_eq_smul_cast]; exact sum_le_card_nsmul _ _ _ h + rw [Nat.cast_smul_eq_nsmul]; exact sum_le_card_nsmul _ _ _ h lemma le_expect (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, a ≤ f x) : a ≤ 𝔼 i ∈ s, f i := (le_inv_smul_iff_of_pos $ by positivity).2 $ by - rw [←nsmul_eq_smul_cast]; exact card_nsmul_le_sum _ _ _ h + rw [Nat.cast_smul_eq_nsmul]; exact card_nsmul_le_sum _ _ _ h lemma expect_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ 𝔼 i ∈ s, f i := smul_nonneg (by positivity) $ sum_nonneg hf diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean index fdde91df3e..627452a264 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean @@ -25,7 +25,7 @@ lemma lpNorm_expect_le [∀ i, Module ℚ≥0 (α i)] (hp : 1 ≤ p) {κ : Type* obtain rfl | hs := s.eq_empty_or_nonempty · simp refine (le_inv_smul_iff_of_pos $ by positivity).2 ?_ - rw [← nsmul_eq_smul_cast, ← lpNorm_nsmul hp, card_smul_expect] + rw [Nat.cast_smul_eq_nsmul, ← lpNorm_nsmul hp, card_smul_expect] exact lpNorm_sum_le hp _ _ end one_le diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean index 1cf979878b..dff4d5769c 100644 --- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean +++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean @@ -127,7 +127,7 @@ variable [∀ i, NormedSpace ℝ (α i)] lemma wlpNorm_nsmul (hp : 1 ≤ p) (n : ℕ) (w : ι → ℝ≥0) (f : ∀ i, α i) : ‖n • f‖_[p, w] = n • ‖f‖_[p, w] := by - rw [nsmul_eq_smul_cast ℝ, wlpNorm_smul hp, RCLike.norm_natCast, nsmul_eq_mul] + rw [← Nat.cast_smul_eq_nsmul ℝ, wlpNorm_smul hp, RCLike.norm_natCast, nsmul_eq_mul] end one_le diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index 4f1666a031..789ab2f518 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -1,12 +1,14 @@ import Mathlib.Analysis.MeanInequalitiesPow -import LeanAPAP.Mathlib.Algebra.BigOperators.Pi +import LeanAPAP.Mathlib.Data.Fintype.BigOperators import LeanAPAP.Prereqs.Multinomial open Finset Fintype Nat Real variable {G : Type*} {A : Finset G} {m n : ℕ} +local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s + private lemma step_one (hA : A.Nonempty) (f : G → ℝ) (a : Fin n → G) - (hf : ∀ i : Fin n, ∑ a in A^^n, f (a i) = 0) : + (hf : ∀ i : Fin n, ∑ a in A ^^ n, f (a i) = 0) : |∑ i, f (a i)| ^ (m + 1) ≤ (∑ b in A^^n, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / A.card ^ n := calc |∑ i, f (a i)| ^ (m + 1) @@ -14,8 +16,8 @@ private lemma step_one (hA : A.Nonempty) (f : G → ℝ) (a : Fin n → G) simp only [hf, sub_zero, zero_div] _ = |(∑ b in A^^n, ∑ i, (f (a i) - f (b i))) / (A^^n).card| ^ (m + 1) := by simp only [sum_sub_distrib] - rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinsetConst, Nat.cast_pow, - mul_div_cancel_left₀] + rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const, + card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀] exact pow_ne_zero _ $ Nat.cast_ne_zero.2 hA.card_pos.ne' _ = |∑ b in A^^n, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / (A^^n).card ^ (m + 1) := by rw [abs_div, div_pow, Nat.abs_cast] @@ -82,7 +84,7 @@ private lemma step_two (f : G → ℝ) : ∑ a in A^^n, ∑ b in A^^n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) = ∑ a in A^^n, ∑ b in A^^n, (∑ i, (f (a i) - f (b i))) ^ (2 * m) := fun ε hε ↦ step_two_aux A f _ hε fun z : Fin n → ℝ ↦ univ.sum z ^ (2 * m) - rw [Finset.sum_congr rfl this, sum_const, card_piFinsetConst, card_pair, nsmul_eq_mul, + rw [Finset.sum_congr rfl this, sum_const, card_piFinset_const, card_pair, nsmul_eq_mul, Nat.cast_pow, Nat.cast_two, inv_pow, inv_mul_cancel_left₀] · positivity · norm_num @@ -93,7 +95,7 @@ private lemma step_three (f : G → ℝ) : ∑ a in A^^n, ∑ b in A^^n, ∑ k in piAntidiag univ (2 * m), (multinomial univ k * ∏ t, (f (a t) - f (b t)) ^ k t) * ∑ ε in ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t := by - simp only [@sum_comm _ _ (Fin n → ℝ) _ _ (A^^n), ←Complex.abs_pow, multinomial_expansion'] + simp only [@sum_comm _ _ (Fin n → ℝ) _ _ (A^^n), ←Complex.abs_pow, sum_pow_eq_sum_piAntidiag] refine sum_congr rfl fun a _ ↦ ?_ refine sum_congr rfl fun b _ ↦ ?_ simp only [mul_pow, prod_mul_distrib, @sum_comm _ _ (Fin n → ℝ), ←mul_sum, ←sum_mul] @@ -103,7 +105,7 @@ private lemma step_three (f : G → ℝ) : private lemma step_four {k : Fin n → ℕ} : ∑ ε in ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t = 2 ^ n * ite (∀ i, Even (k i)) 1 0 := by have := sum_prod_piFinset ({-1, 1} : Finset ℝ) fun i fi ↦ fi ^ k i - rw [piFinsetConst, this, ←Fintype.prod_boole] + rw [this, ←Fintype.prod_boole] have : (2 : ℝ) ^ n = ∏ i : Fin n, 2 := by simp rw [this, ←prod_mul_distrib] refine prod_congr rfl fun t _ ↦ ?_ @@ -121,7 +123,7 @@ private lemma step_six {f : G → ℝ} {a b : Fin n → G} : ∑ k : Fin n → ℕ in piAntidiag univ m, (multinomial univ fun a ↦ 2 * k a : ℝ) * ∏ i : Fin n, (f (a i) - f (b i)) ^ (2 * k i) ≤ m ^ m * (∑ i : Fin n, (f (a i) - f (b i)) ^ 2) ^ m := by - rw [multinomial_expansion', mul_sum] + rw [sum_pow_eq_sum_piAntidiag, mul_sum] convert sum_le_sum fun k hk ↦ _ rw [mem_piAntidiag] at hk simp only [←mul_assoc, pow_mul] @@ -169,8 +171,8 @@ private lemma end_step {f : G → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) : _ = _ := by simp only [mul_add, sum_add_distrib, sum_const, nsmul_eq_mul, ←mul_sum] rw [←mul_add, ←two_mul, ←mul_assoc 2, ←mul_assoc 2, mul_right_comm 2, ←_root_.pow_succ', - add_assoc, Nat.sub_add_cancel hm, pow_add, ←mul_pow, ←mul_pow, card_piFinsetConst, - Nat.cast_pow, mul_div_cancel_left₀] + add_assoc, Nat.sub_add_cancel hm, pow_add, ←mul_pow, ←mul_pow, card_piFinset, prod_const, + card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀] norm_num · have := hA.card_pos positivity @@ -184,7 +186,7 @@ lemma basic_marcinkiewicz_zygmund (f : G → ℝ) (hf : ∀ i : Fin n, ∑ a in rcases A.eq_empty_or_nonempty with (rfl | hA) · cases n · cases m <;> simp - · rw [piFinsetConst, piFinset_empty, Finset.sum_empty] + · rw [piFinset_empty, Finset.sum_empty] cases m <;> simp refine (sum_le_sum fun a (_ : a ∈ A^^n) ↦ @step_one' _ _ _ _ hA f hf a).trans ?_ rw [←sum_div] diff --git a/LeanAPAP/Prereqs/Multinomial.lean b/LeanAPAP/Prereqs/Multinomial.lean index ca81a990d5..c85bb51f81 100644 --- a/LeanAPAP/Prereqs/Multinomial.lean +++ b/LeanAPAP/Prereqs/Multinomial.lean @@ -1,50 +1,11 @@ -import Mathlib.Algebra.Order.Antidiag.Finsupp import Mathlib.Data.Nat.Choose.Multinomial import Mathlib.Data.Nat.Factorial.DoubleFactorial -open Finset Nat - -open scoped Nat +open Finset variable {K : Type*} {s : Finset K} {f f' : K → ℕ} - namespace Nat -lemma multinomial_expansion' {α β : Type*} [DecidableEq α] [CommSemiring β] {s : Finset α} - {x : α → β} {n : ℕ} : - (∑ i in s, x i) ^ n = ∑ k in piAntidiag s n, multinomial s k * ∏ t in s, x t ^ k t := by - classical - induction' s using Finset.cons_induction with a s has ih generalizing n - · cases n <;> simp - rw [Finset.sum_cons, piAntidiag_cons, sum_disjiUnion] - simp only [sum_map, Function.Embedding.coeFn_mk, Pi.add_apply, multinomial_cons, - Pi.add_apply, eq_self_iff_true, if_true, Nat.cast_mul, prod_cons, eq_self_iff_true, - if_true, sum_add_distrib, sum_ite_eq', has, if_false, add_zero, - addLeftEmbedding_eq_addRightEmbedding, addRightEmbedding_apply] - suffices ∀ p : ℕ × ℕ, p ∈ antidiagonal n → - ∑ f in piAntidiag s p.2, ((f a + p.1 + s.sum f).choose (f a + p.1) : β) * - multinomial s (f + fun t ↦ ite (t = a) p.1 0) * - (x a ^ (f a + p.1) * ∏ t in s, x t ^ (f t + ite (t = a) p.1 0)) = - ∑ f in piAntidiag s p.2, n.choose p.1 * multinomial s f * (x a ^ p.1 * ∏ t in s, x t ^ f t) by - rw [sum_congr rfl this] - simp only [Nat.antidiagonal_eq_map, sum_map, Function.Embedding.coeFn_mk] - rw [add_pow] - simp only [ih, sum_mul, mul_sum] - refine sum_congr rfl fun i _ ↦ sum_congr rfl fun f _ ↦ ?_ - ac_rfl - refine fun p hp ↦ sum_congr rfl fun f hf ↦ ?_ - rw [mem_piAntidiag] at hf - rw [not_imp_comm.1 (hf.2 _) has, zero_add, hf.1] - congr 2 - · rw [mem_antidiagonal.1 hp] - · rw [multinomial_congr] - intro t ht - rw [Pi.add_apply, if_neg, add_zero] - exact ne_of_mem_of_not_mem ht has - refine prod_congr rfl fun t ht ↦ ?_ - rw [if_neg, add_zero] - exact ne_of_mem_of_not_mem ht has - lemma double_multinomial : (multinomial s fun i ↦ 2 * f i) ≤ ((∑ i in s, f i) ^ ∑ i in s, f i) * multinomial s f := by rw [multinomial, multinomial, ←mul_sum] diff --git a/lake-manifest.json b/lake-manifest.json index bb4918ef35..3d960ab31f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592", + "rev": "e7897807913fafdab31b01b9f627550bcc96cff2", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c", + "rev": "79fb157c6a5061190d169535f8e5cb007914a82e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "c87908619cccadda23f71262e6898b9893bffa36", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.40", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "63341a2ea2f7c99ff4315e13c763dca1bfd13d7d", + "rev": "bb85073b9fa01e154556d21eec50f489f730b253", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,