From fc640cc277463e9cd70c391f62a37a4fb37e303d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 20 Sep 2024 20:58:18 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 3 +- .../Group/Pointwise/Finset.lean} | 2 +- LeanAPAP/Mathlib/Data/Fintype/Basic.lean | 3 + .../MeasureTheory/Function/EssSup.lean | 1 - LeanAPAP/Physics/AlmostPeriodicity.lean | 4 +- LeanAPAP/Physics/DRC.lean | 8 +- LeanAPAP/Physics/Unbalancing.lean | 4 +- LeanAPAP/Prereqs/AddChar/Basic.lean | 2 +- LeanAPAP/Prereqs/Balance.lean | 2 +- LeanAPAP/Prereqs/Convolution/Compact.lean | 2 + LeanAPAP/Prereqs/Expect/Basic.lean | 352 +----------------- LeanAPAP/Prereqs/Expect/MeanInequalities.lean | 2 +- LeanAPAP/Prereqs/Expect/Order.lean | 23 +- .../Prereqs/Function/Indicator/Basic.lean | 3 +- LeanAPAP/Prereqs/Function/Indicator/Defs.lean | 2 +- LeanAPAP/Prereqs/Inner/Function.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Compact.lean | 1 + LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean | 2 - LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 4 +- LeanAPAP/Prereqs/NNLpNorm.lean | 2 +- LeanAPAP/Prereqs/PointwiseDensity.lean | 2 +- lake-manifest.json | 16 +- 22 files changed, 53 insertions(+), 389 deletions(-) rename LeanAPAP/Mathlib/{Data/Finset/Pointwise/Basic.lean => Algebra/Group/Pointwise/Finset.lean} (85%) create mode 100644 LeanAPAP/Mathlib/Data/Fintype/Basic.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index dc5c086c19..c1dc7abf71 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -4,6 +4,7 @@ import LeanAPAP.Integer import LeanAPAP.Mathlib.Algebra.BigOperators.Group.Finset import LeanAPAP.Mathlib.Algebra.Group.AddChar import LeanAPAP.Mathlib.Algebra.Group.Basic +import LeanAPAP.Mathlib.Algebra.Group.Pointwise.Finset import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset import LeanAPAP.Mathlib.Algebra.Order.Field.Defs @@ -24,8 +25,8 @@ import LeanAPAP.Mathlib.Data.ENNReal.Basic import LeanAPAP.Mathlib.Data.ENNReal.Operations import LeanAPAP.Mathlib.Data.ENNReal.Real import LeanAPAP.Mathlib.Data.Finset.Density -import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic import LeanAPAP.Mathlib.Data.Finset.Preimage +import LeanAPAP.Mathlib.Data.Fintype.Basic import LeanAPAP.Mathlib.Data.Real.ConjExponents import LeanAPAP.Mathlib.Data.ZMod.Module import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup diff --git a/LeanAPAP/Mathlib/Data/Finset/Pointwise/Basic.lean b/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean similarity index 85% rename from LeanAPAP/Mathlib/Data/Finset/Pointwise/Basic.lean rename to LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean index c532082453..90f2073173 100644 --- a/LeanAPAP/Mathlib/Data/Finset/Pointwise/Basic.lean +++ b/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean @@ -1,5 +1,5 @@ +import Mathlib.Algebra.Group.Pointwise.Finset.Basic import Mathlib.Data.Finset.Density -import Mathlib.Data.Finset.Pointwise.Basic open scoped Pointwise diff --git a/LeanAPAP/Mathlib/Data/Fintype/Basic.lean b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean new file mode 100644 index 0000000000..2920eebb80 --- /dev/null +++ b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean @@ -0,0 +1,3 @@ +import Mathlib.Data.Fintype.Basic + +attribute [simp] Finset.univ_nonempty diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean index 5f1fc2451f..2a8335967c 100644 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean +++ b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean @@ -1,6 +1,5 @@ import Mathlib.MeasureTheory.Function.EssSup import Mathlib.Probability.ConditionalProbability -import LeanAPAP.Mathlib.MeasureTheory.Measure.Count open Filter MeasureTheory ProbabilityTheory open scoped ENNReal diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index d39f62cea6..b0a33275ed 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -200,7 +200,7 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0) ∃ a : Fin k → G, a ∈ L ∧ L.card * S.card ≤ (A + S).card ^ k * (univ.filter fun t : G ↦ (a - fun _ ↦ t) ∈ L).card := by rcases S.eq_empty_or_nonempty with (rfl | hS) - · simpa only [card_empty, mul_zero, zero_le', and_true_iff] using hL' + · simpa only [card_empty, mul_zero, zero_le', and_true] using hL' 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 ?_ @@ -421,7 +421,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) ( exact T_bound hK₂ L.card S.card A.card (A + S).card _ rfl hL' this (by rw [← cast_addConst_mul_card]; gcongr) hA.card_pos hε hε' hm intro t ht - simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and_iff] at ht + simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and] at ht have := just_the_triangle_inequality ha ht hk.bot_lt hm rwa [neg_neg, mul_div_cancel₀ _ (two_ne_zero' ℝ)] at this diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 8a363c5242..3c3457c47c 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -94,7 +94,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ (dconv_nonneg indicate_nonneg indicate_nonneg) _) fun _ ↦ by simp -- positivity refine Fintype.sum_pos $ this.gt_iff_ne.2 $ support_nonempty_iff.1 ?_ simp only [support_comp_eq, Set.Nonempty, and_assoc, support_mul', support_dconv, - indicate_nonneg, mu_nonneg, support_indicate, support_mu, NNReal.coe_eq_zero, iff_self_iff, + indicate_nonneg, mu_nonneg, support_indicate, support_mu, NNReal.coe_eq_zero, iff_self, forall_const, Set.mem_inter_iff, ← coe_sub, mem_coe, support_pow' _ hp₀, hf] set A₁ := fun s ↦ B₁ ∩ c p A s set A₂ := fun s ↦ B₂ ∩ c p A s @@ -111,7 +111,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ (2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x) by obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩ - simp only [indicate_apply, mem_filter, mem_univ, true_and_iff, boole_mul] at hs + simp only [indicate_apply, mem_filter, mem_univ, true_and, boole_mul] at hs split_ifs at hs with h; swap · simp only [zero_mul, dL2Inner_eq_sum, Function.comp_apply, RCLike.inner_apply, RCLike.conj_to_real] at hs @@ -133,7 +133,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB, mul_left_comm, ← mul_assoc] - simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and_iff, ← sum_filter, + simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and, ← sum_filter, mul_lt_mul_right hf, Function.comp_apply] by_cases h : ∀ s, g s ≠ 0 → M ^ 2 ≤ g s · rw [← sum_filter_ne_zero (s := filter _ _), Finset.filter_comm, @@ -161,7 +161,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ := mul_le_mul_of_nonneg_left (sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity) hM.le _ = _ := ?_ - · simp only [mem_filter, mem_univ, true_and_iff, Nat.cast_nonneg, and_imp] + · simp only [mem_filter, mem_univ, true_and, Nat.cast_nonneg, and_imp] exact fun s hsM hs ↦ mul_lt_mul_of_pos_right ((sqrt_lt' hM).2 hsM) $ sqrt_pos.2 $ (hg _).lt_of_ne' hs rw [sum_cast_c, sum_cast_c, sqrt_mul', sqrt_mul', mul_mul_mul_comm (sqrt _), mul_self_sqrt, diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index fe965a2f9b..cae9fa5bbc 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -34,7 +34,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ g = f) (hν : h ○ h = (↑ have : ∀ x, ∀ yz ∈ univ.filter fun yz : G × G ↦ yz.1 - yz.2 = x, conj ((g ○ g) x) ^ k * (h yz.1 * conj (h yz.2)) = conj ((g ○ g) (yz.1 - yz.2)) ^ k * (h yz.1 * conj (h yz.2)) := by - simp only [mem_filter, mem_univ, true_and_iff] + simp only [mem_filter, mem_univ, true_and] rintro _ _ rfl rfl refine (sum_congr rfl fun _ _ ↦ sum_congr rfl $ this _).trans ?_ @@ -121,7 +121,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 _ = (3 / 4) ^ p * ε ^ p * ∑ i in P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow] _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_ _ = 4⁻¹ * ε ^ p := by norm_cast; simp [hν₁] - · simp only [mem_sdiff, mem_filter, mem_univ, true_and_iff, not_le, P, T] at hi + · simp only [mem_sdiff, mem_filter, mem_univ, true_and, not_le, P, T] at hi exact mul_le_mul_of_nonneg_left (pow_le_pow_left hi.1 hi.2.le _) (by positivity) · refine mul_le_mul (mul_le_mul_of_nonneg_right (le_trans (pow_le_pow_of_le_one ?_ ?_ hp) ?_) ?_) (sum_le_univ_sum_of_nonneg fun i ↦ ?_) ?_ ?_ <;> diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean index 54e14192be..771b865f13 100644 --- a/LeanAPAP/Prereqs/AddChar/Basic.lean +++ b/LeanAPAP/Prereqs/AddChar/Basic.lean @@ -1,5 +1,5 @@ +import Mathlib.Algebra.BigOperators.Expect import LeanAPAP.Mathlib.Algebra.Group.AddChar -import LeanAPAP.Prereqs.Expect.Basic import LeanAPAP.Prereqs.Inner.Discrete.Defs open Finset hiding card diff --git a/LeanAPAP/Prereqs/Balance.lean b/LeanAPAP/Prereqs/Balance.lean index c22d984b5b..0e59941f8f 100644 --- a/LeanAPAP/Prereqs/Balance.lean +++ b/LeanAPAP/Prereqs/Balance.lean @@ -1,4 +1,4 @@ -import LeanAPAP.Prereqs.Expect.Basic +import Mathlib.Algebra.BigOperators.Expect /-! # Balancing a function diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean index 90e9924fa2..d8ef1f22b6 100644 --- a/LeanAPAP/Prereqs/Convolution/Compact.lean +++ b/LeanAPAP/Prereqs/Convolution/Compact.lean @@ -1,4 +1,6 @@ +import LeanAPAP.Mathlib.Data.Fintype.Basic import LeanAPAP.Prereqs.Convolution.Discrete.Defs +import LeanAPAP.Prereqs.Expect.Basic import LeanAPAP.Prereqs.Expect.Complex import LeanAPAP.Prereqs.Function.Indicator.Defs diff --git a/LeanAPAP/Prereqs/Expect/Basic.lean b/LeanAPAP/Prereqs/Expect/Basic.lean index e06c3cd41c..d90e62e50f 100644 --- a/LeanAPAP/Prereqs/Expect/Basic.lean +++ b/LeanAPAP/Prereqs/Expect/Basic.lean @@ -3,14 +3,10 @@ Copyright (c) 2024 Yaël Dillies, Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies, Bhavik Mehta -/ -import Mathlib.Algebra.Algebra.Rat -import Mathlib.Algebra.BigOperators.GroupWithZero.Action +import Mathlib.Algebra.BigOperators.Expect import Mathlib.Algebra.BigOperators.Pi -import Mathlib.Algebra.BigOperators.Ring import Mathlib.Algebra.Module.Pi import Mathlib.Data.Finset.Density -import Mathlib.Data.Finset.Pointwise.Basic -import Mathlib.Data.Fintype.BigOperators /-! # Average over a finset @@ -34,120 +30,15 @@ Connect `Finset.expect` with the expectation over `s` in the probability theory open Finset Function open Fintype (card) -open scoped Pointwise +open scoped BigOperators Pointwise variable {ι κ M N : Type*} -local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a - -/-- Average of a function over a finset. If the finset is empty, this is equal to zero. -/ -def Finset.expect [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : M := - (s.card : ℚ≥0)⁻¹ • ∑ i ∈ s, f i - -namespace BigOperators -open Batteries.ExtendedBinder Lean Meta - -/-- -* `𝔼 i ∈ s, f i` is notation for `Finset.expect s f`. It is the expectation of `f i` where `i` - ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance). -* `𝔼 i, f i` is notation for `Finset.expect Finset.univ f`. It is the expectation of `f i` where `i` - ranges over the finite domain of `f`. -* `𝔼 i ∈ s with p i, f i` is notation for `Finset.expect (Finset.filter p s) f`. -* `𝔼 (i ∈ s) (j ∈ t), f i j` is notation for `Finset.expect (s ×ˢ t) (fun ⟨i, j⟩ ↦ f i j)`. - -These support destructuring, for example `𝔼 ⟨i, j⟩ ∈ s ×ˢ t, f i j`. - -Notation: `"𝔼" bigOpBinders* ("with" term)? "," term` -/ -scoped syntax (name := bigexpect) "𝔼 " bigOpBinders ("with " term)? ", " term:67 : term - -scoped macro_rules (kind := bigexpect) - | `(𝔼 $bs:bigOpBinders $[with $p?]?, $v) => do - let processed ← processBigOpBinders bs - let i ← bigOpBindersPattern processed - let s ← bigOpBindersProd processed - match p? with - | some p => `(Finset.expect (Finset.filter (fun $i ↦ $p) $s) (fun $i ↦ $v)) - | none => `(Finset.expect $s (fun $i ↦ $v)) - -open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr -open Batteries.ExtendedBinder - -/-- Delaborator for `Finset.expect`. The `pp.piBinderTypes` option controls whether -to show the domain type when the expect is over `Finset.univ`. -/ -@[scoped delab app.Finset.expect] def delabFinsetExpect : Delab := - whenPPOption getPPNotation <| withOverApp 6 <| do - let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure - guard <| f.isLambda - let ppDomain ← getPPOption getPPPiBinderTypes - let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do - return (i, ← delab) - if s.isAppOfArity ``Finset.univ 2 then - let binder ← - if ppDomain then - let ty ← withNaryArg 0 delab - `(bigOpBinder| $(.mk i):ident : $ty) - else - `(bigOpBinder| $(.mk i):ident) - `(𝔼 $binder:bigOpBinder, $body) - else - let ss ← withNaryArg 4 <| delab - `(𝔼 $(.mk i):ident ∈ $ss, $body) - -end BigOperators - -open scoped BigOperators - namespace Finset section AddCommMonoid variable [AddCommMonoid M] [Module ℚ≥0 M] [AddCommMonoid N] [Module ℚ≥0 N] {s t : Finset ι} {f g : ι → M} {m : N → M} {p q : ι → Prop} [DecidablePred p] [DecidablePred q] -lemma expect_univ [Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι := by - rw [expect, card_univ] - -@[simp] lemma expect_empty (f : ι → M) : 𝔼 i ∈ ∅, f i = 0 := by simp [expect] -@[simp] lemma expect_singleton (f : ι → M) (i : ι) : 𝔼 j ∈ {i}, f j = f i := by simp [expect] -@[simp] lemma expect_const_zero (s : Finset ι) : 𝔼 _i ∈ s, (0 : M) = 0 := by simp [expect] - -@[congr] -lemma expect_congr {t : Finset ι} (hst : s = t) (h : ∀ i ∈ t, f i = g i) : - 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by rw [expect, expect, sum_congr hst h, hst] - -lemma expectWith_congr (hst : s = t) (hpq : ∀ i ∈ t, p i ↔ q i) (h : ∀ i ∈ t, q i → f i = g i) : - 𝔼 i ∈ s with p i, f i = 𝔼 i ∈ t with q i, g i := - expect_congr (by rw [hst, (filter_inj' ..).2 hpq]) <| by simpa using h - -lemma expect_sum_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : - 𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j := by - simpa only [expect, smul_sum] using sum_comm - -lemma expect_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) : - 𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j := by - rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm] - -lemma expect_eq_zero (h : ∀ i ∈ s, f i = 0) : 𝔼 i ∈ s, f i = 0 := - (expect_congr rfl h).trans s.expect_const_zero - -lemma exists_ne_zero_of_expect_ne_zero (h : 𝔼 i ∈ s, f i ≠ 0) : ∃ i ∈ s, f i ≠ 0 := by - contrapose! h; exact expect_eq_zero h - -lemma expect_add_distrib (s : Finset ι) (f g : ι → M) : - 𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i := by - simp [expect, sum_add_distrib] - -lemma expect_add_expect_comm (f₁ f₂ g₁ g₂ : ι → M) : - 𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) = - 𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i) := by - simp_rw [expect_add_distrib, add_add_add_comm] - -lemma expect_eq_single_of_mem (i : ι) (hi : i ∈ s) (h : ∀ j ∈ s, j ≠ i → f j = 0) : - 𝔼 i ∈ s, f i = f i /ℚ s.card := by rw [expect, sum_eq_single_of_mem _ hi h] - -lemma expect_ite_zero (s : Finset ι) (p : ι → Prop) [DecidablePred p] - (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) : - 𝔼 i ∈ s, ite (p i) a 0 = ite (∃ i ∈ s, p i) (a /ℚ s.card) 0 := by - split_ifs <;> simp [expect, sum_ite_zero _ _ h, *] - section DecidableEq variable [DecidableEq ι] @@ -157,267 +48,30 @@ variable [DecidableEq ι] · simp [expect, hst] · simp [expect, smul_smul, ← inv_mul_eq_div, hst.card_ne_zero] -@[simp] lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) : - 𝔼 j ∈ s, (if h : i = j then f j h else 0) = if i ∈ s then f i rfl /ℚ s.card else 0 := by - split_ifs <;> simp [expect, *] - -@[simp] lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) : - 𝔼 j ∈ s, (if h : j = i then f j h else 0) = if i ∈ s then f i rfl /ℚ s.card else 0 := by - split_ifs <;> simp [expect, *] - -@[simp] lemma expect_ite_eq (i : ι) (f : ι → M) : - 𝔼 j ∈ s, (if i = j then f j else 0) = if i ∈ s then f i /ℚ s.card else 0 := by - split_ifs <;> simp [expect, *] - -@[simp] lemma expect_ite_eq' (i : ι) (f : ι → M) : - 𝔼 j ∈ s, (if j = i then f j else 0) = if i ∈ s then f i /ℚ s.card else 0 := by - split_ifs <;> simp [expect, *] - end DecidableEq - -section bij -variable {t : Finset κ} {g : κ → M} - -/-- Reorder an average. - -The difference with `Finset.expect_bij'` is that the bijection is specified as a surjective -injection, rather than by an inverse function. - -The difference with `Finset.expect_nbij` is that the bijection is allowed to use membership of the -domain of the average, rather than being a non-dependent function. -/ -lemma expect_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha)) - (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) - (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by - simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h] - -/-- Reorder an average. - -The difference with `Finset.expect_bij` is that the bijection is specified with an inverse, rather -than as a surjective injection. - -The difference with `Finset.expect_nbij'` is that the bijection and its inverse are allowed to use -membership of the domains of the averages, rather than being non-dependent functions. -/ -lemma expect_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t) - (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) - (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) : - 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by - simp_rw [expect, card_bij' i j hi hj left_inv right_inv, sum_bij' i j hi hj left_inv right_inv h] - -/-- Reorder an average. - -The difference with `Finset.expect_nbij'` is that the bijection is specified as a surjective -injection, rather than by an inverse function. - -The difference with `Finset.expect_bij` is that the bijection is a non-dependent function, rather -than being allowed to use membership of the domain of the average. -/ -lemma expect_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) - (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t) : - 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by - simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h] - -/-- Reorder an average. - -The difference with `Finset.expect_nbij` is that the bijection is specified with an inverse, rather -than as a surjective injection. - -The difference with `Finset.expect_bij'` is that the bijection and its inverse are non-dependent -functions, rather than being allowed to use membership of the domains of the averages. - -The difference with `Finset.expect_equiv` is that bijectivity is only required to hold on the -domains of the averages, rather than on the entire types. -/ -lemma expect_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) - (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) - (h : ∀ a ∈ s, f a = g (i a)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by - simp_rw [expect, card_nbij' i j hi hj left_inv right_inv, - sum_nbij' i j hi hj left_inv right_inv h] - -/-- `Finset.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in -most arguments. -/ -lemma expect_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : - 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg] - -lemma expect_product (f : ι × κ → M) : 𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j) := by - simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul] - -lemma expect_product' (f : ι → κ → M) : 𝔼 i ∈ s ×ˢ t, f i.1 i.2 = 𝔼 i ∈ s, 𝔼 j ∈ t, f i j := by - simp only [expect, card_product, sum_product', smul_sum, mul_inv, mul_smul, Nat.cast_mul] - -@[simp] -lemma expect_image [DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m) : - 𝔼 i ∈ t.image m, f i = 𝔼 i ∈ t, f (m i) := by - simp_rw [expect, card_image_of_injOn hm, sum_image hm] - -end bij - -@[simp] lemma expect_inv_index [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) : - 𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹ := expect_image inv_injective.injOn - -@[simp] lemma expect_neg_index [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) : - 𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) := expect_image neg_injective.injOn - -lemma _root_.map_expect {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N] - (g : F) (f : ι → M) (s : Finset ι) : - g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i) := by simp only [expect, map_smul, map_natCast, map_sum] - -@[simp] -lemma card_smul_expect (s : Finset ι) (f : ι → M) : s.card • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by - obtain rfl | hs := s.eq_empty_or_nonempty - · simp - · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀] - exact mod_cast hs.card_ne_zero - -@[simp] lemma _root_.Fintype.card_smul_expect [Fintype ι] (f : ι → M) : - Fintype.card ι • 𝔼 i, f i = ∑ i, f i := Finset.card_smul_expect _ _ - -@[simp] lemma expect_const (hs : s.Nonempty) (a : M) : 𝔼 _i ∈ s, a = a := by - rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀] - exact mod_cast hs.card_ne_zero - -lemma smul_expect {G : Type*} [DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G) - (s : Finset ι) (f : ι → M) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by - simp only [expect, smul_sum, smul_comm] - end AddCommMonoid -section AddCommGroup -variable [AddCommGroup M] [Module ℚ≥0 M] [Field N] [Module ℚ≥0 N] {s : Finset ι} - -lemma expect_sub_distrib (s : Finset ι) (f g : ι → M) : - 𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i := by - simp only [expect, sum_sub_distrib, smul_sub] - -@[simp] -lemma expect_neg_distrib (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i := by - simp [expect] - -end AddCommGroup - -section Semiring -variable [Semiring M] [Module ℚ≥0 M] {s : Finset ι} {f g : ι → M} {m : N → M} - -@[simp] lemma card_mul_expect (s : Finset ι) (f : ι → M) : - s.card * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by rw [← nsmul_eq_mul, card_smul_expect] - -@[simp] lemma _root_.Fintype.card_mul_expect [Fintype ι] (f : ι → M) : - Fintype.card ι * 𝔼 i, f i = ∑ i, f i := Finset.card_mul_expect _ _ - -lemma expect_mul [IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : - (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a := by rw [expect, expect, smul_mul_assoc, sum_mul] - -lemma mul_expect [SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : - a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i := by rw [expect, expect, mul_smul_comm, mul_sum] - -lemma expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι) - (t : Finset κ) (f : ι → M) (g : κ → M) : - (𝔼 i ∈ s, f i) * 𝔼 j ∈ t, g j = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j := by - simp_rw [expect_mul, mul_expect] - -end Semiring - -section CommSemiring -variable [CommSemiring M] [Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] - -lemma expect_pow (s : Finset ι) (f : ι → M) (n : ℕ) : - (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun _ : Fin n ↦ s, ∏ i, f (p i) := by - classical - rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow] - -end CommSemiring - -section Semifield -variable [Semifield M] [CharZero M] {s : Finset ι} {f g : ι → M} {m : N → M} - -lemma expect_boole_mul [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) : - 𝔼 j, ite (i = j) (Fintype.card ι : M) 0 * f j = f i := by - simp_rw [expect_univ, ite_mul, zero_mul, sum_ite_eq, if_pos (mem_univ _)] - rw [← @NNRat.cast_natCast M, ← NNRat.smul_def, inv_smul_smul₀] - simp [Fintype.card_ne_zero] - -lemma expect_boole_mul' [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) : - 𝔼 j, ite (j = i) (Fintype.card ι : M) 0 * f j = f i := by - simp_rw [@eq_comm _ _ i, expect_boole_mul] - -lemma expect_eq_sum_div_card (s : Finset ι) (f : ι → M) : - 𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / s.card := by - rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast] - -lemma _root_.Fintype.expect_eq_sum_div_card [Fintype ι] (f : ι → M) : - 𝔼 i, f i = (∑ i, f i) / Fintype.card ι := Finset.expect_eq_sum_div_card _ _ - -lemma expect_div (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a := by - simp_rw [div_eq_mul_inv, expect_mul] - -end Semifield - @[simp] lemma expect_apply {α : Type*} {π : α → Type*} [∀ a, CommSemiring (π a)] [∀ a, Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → ∀ a, π a) (a : α) : (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a := by simp [expect] end Finset -namespace algebraMap -variable [Semifield M] [CharZero M] [Semifield N] [CharZero N] [Algebra M N] - -@[simp, norm_cast] -lemma coe_expect (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : N) := - map_expect (algebraMap _ _) _ _ - -end algebraMap - namespace Fintype variable [Fintype ι] [Fintype κ] section AddCommMonoid -variable [AddCommMonoid M] [Module ℚ≥0 M] {f : ι → M} - -/-- `Fintype.expect_bijective` is a variant of `Finset.expect_bij` that accepts -`Function.Bijective`. - -See `Function.Bijective.expect_comp` for a version without `h`. -/ -lemma expect_bijective (e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M) - (h : ∀ i, f i = g (e i)) : 𝔼 i, f i = 𝔼 i, g i := - expect_nbij e (fun _ _ ↦ mem_univ _) (fun i _ ↦ h i) he.injective.injOn <| by - simpa using he.surjective.surjOn _ - -/-- `Fintype.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in -most arguments. - -See `Equiv.expect_comp` for a version without `h`. -/ -lemma expect_equiv (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ i, f i = g (e i)) : - 𝔼 i, f i = 𝔼 i, g i := expect_bijective _ e.bijective f g h - -@[simp] lemma expect_const [Nonempty ι] (a : M) : 𝔼 _i : ι, a = a := - Finset.expect_const univ_nonempty _ - -lemma expect_ite_zero (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) : - 𝔼 i, ite (p i) a 0 = ite (∃ i, p i) (a /ℚ Fintype.card ι) 0 := by - simp [univ.expect_ite_zero p (by simpa using h), card_univ] - -variable [DecidableEq ι] +variable [AddCommMonoid M] [Module ℚ≥0 M] {f : ι → M} [DecidableEq ι] @[simp] lemma expect_ite_mem (s : Finset ι) (f : ι → M) : 𝔼 i, (if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i := by simp [Finset.expect_ite_mem, dens] -lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) : - 𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι := by simp [card_univ] - -lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) : - 𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι := by simp [card_univ] - -lemma expect_ite_eq (i : ι) (f : ι → M) : - 𝔼 j, (if i = j then f j else 0) = f i /ℚ card ι := by simp [card_univ] - -lemma expect_ite_eq' (i : ι) (f : ι → M) : - 𝔼 j, (if j = i then f j else 0) = f i /ℚ card ι := by simp [card_univ] - end AddCommMonoid section Semiring variable [Semiring M] [Module ℚ≥0 M] -@[simp] lemma expect_one [Nonempty ι] : 𝔼 _i : ι, (1 : M) = 1 := expect_const _ - lemma expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (f : ι → M) (g : κ → M) : (𝔼 i, f i) * 𝔼 j, g j = 𝔼 i, 𝔼 j, f i * g j := Finset.expect_mul_expect .. diff --git a/LeanAPAP/Prereqs/Expect/MeanInequalities.lean b/LeanAPAP/Prereqs/Expect/MeanInequalities.lean index c22fbe51d5..07069cada6 100644 --- a/LeanAPAP/Prereqs/Expect/MeanInequalities.lean +++ b/LeanAPAP/Prereqs/Expect/MeanInequalities.lean @@ -1,5 +1,5 @@ +import Mathlib.Algebra.BigOperators.Expect import Mathlib.Analysis.MeanInequalities -import LeanAPAP.Prereqs.Expect.Basic open Finset open scoped BigOperators diff --git a/LeanAPAP/Prereqs/Expect/Order.lean b/LeanAPAP/Prereqs/Expect/Order.lean index b0e002c26a..4c430ccb37 100644 --- a/LeanAPAP/Prereqs/Expect/Order.lean +++ b/LeanAPAP/Prereqs/Expect/Order.lean @@ -1,15 +1,9 @@ -import Mathlib.Data.Real.Basic -import Mathlib.Algebra.Algebra.Rat -import Mathlib.Algebra.BigOperators.GroupWithZero.Action -import Mathlib.Algebra.BigOperators.Ring -import Mathlib.Algebra.CharP.Defs +import Mathlib.Algebra.BigOperators.Expect import Mathlib.Algebra.Module.Rat import Mathlib.Algebra.Order.BigOperators.Ring.Finset import Mathlib.Algebra.Order.Module.Rat -import Mathlib.Data.Finset.Pointwise.Basic -import Mathlib.Data.Fintype.BigOperators import Mathlib.Data.NNRat.Order -import LeanAPAP.Prereqs.Expect.Basic +import Mathlib.Tactic.GCongr /-! # Order properties of the average over a finset @@ -103,8 +97,9 @@ variable [LinearOrderedCommSemiring R] [ExistsAddOfLE R] [Module ℚ≥0 R] [Pos lemma expect_mul_sq_le_sq_mul_sq (s : Finset ι) (f g : ι → R) : (𝔼 i ∈ s, f i * g i) ^ 2 ≤ (𝔼 i ∈ s, f i ^ 2) * 𝔼 i ∈ s, g i ^ 2 := by simp only [expect, smul_pow, inv_pow, smul_mul_smul_comm, ← sq] + have : (0 : ℚ) ≤ (s.card ^ 2 : ℚ)⁻¹ := by positivity gcongr - exact sum_mul_sq_le_sq_mul_sq .. + exact sum_mul_sq_le_sq_mul_sq (R := R) .. end LinearOrderedCommSemiring end Finset @@ -165,11 +160,11 @@ def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do | _, _ => pure .none | _ => throwError "not Finset.expect" -example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity -example (a : ULift.{2} ℕ → ℝ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity -example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j : Fin 8, 𝔼 i ∈ range n, (a j^2 + i ^ 2) := by positivity -example (n : ℕ) (a : ℕ → ℝ) : 0 < 𝔼 j : Fin (n + 1), (a j^2 + 1) := by positivity -example (a : ℕ → ℝ) : 0 < 𝔼 j ∈ ({1} : Finset ℕ), (a j^2 + 1) := by +example (n : ℕ) (a : ℕ → ℚ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity +example (a : ULift.{2} ℕ → ℚ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity +example (n : ℕ) (a : ℕ → ℚ) : 0 ≤ 𝔼 j : Fin 8, 𝔼 i ∈ range n, (a j^2 + i ^ 2) := by positivity +example (n : ℕ) (a : ℕ → ℚ) : 0 < 𝔼 j : Fin (n + 1), (a j^2 + 1) := by positivity +example (a : ℕ → ℚ) : 0 < 𝔼 j ∈ ({1} : Finset ℕ), (a j^2 + 1) := by have : Finset.Nonempty {1} := singleton_nonempty 1 positivity diff --git a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean index bf4dcacaa7..43343ab2f2 100644 --- a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean +++ b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean @@ -1,7 +1,8 @@ import Mathlib.Algebra.AddTorsor +import Mathlib.Algebra.BigOperators.Expect import Mathlib.Algebra.Star.Conjneg import Mathlib.Data.Fintype.Lattice -import LeanAPAP.Prereqs.Expect.Basic +import Mathlib.Data.NNRat.Order import LeanAPAP.Prereqs.Function.Translate import LeanAPAP.Prereqs.Function.Indicator.Defs diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean index 762ff2f034..bbc1199109 100644 --- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean +++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean @@ -1,8 +1,8 @@ import Mathlib.Algebra.BigOperators.GroupWithZero.Finset import Mathlib.Algebra.BigOperators.Pi +import Mathlib.Algebra.Group.Pointwise.Finset.Basic import Mathlib.Algebra.Order.Field.Defs import Mathlib.Algebra.Star.Pi -import Mathlib.Data.Finset.Pointwise.Basic import Mathlib.Data.Fintype.Lattice import Mathlib.Data.Nat.Cast.Order.Ring diff --git a/LeanAPAP/Prereqs/Inner/Function.lean b/LeanAPAP/Prereqs/Inner/Function.lean index ec73d9a684..e6961308d2 100644 --- a/LeanAPAP/Prereqs/Inner/Function.lean +++ b/LeanAPAP/Prereqs/Inner/Function.lean @@ -1,4 +1,4 @@ -import LeanAPAP.Prereqs.Expect.Basic +import Mathlib.Algebra.BigOperators.Expect import LeanAPAP.Prereqs.Function.Indicator.Defs import LeanAPAP.Prereqs.Inner.Discrete.Defs diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean index 8ce3b62686..594984cbdb 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean @@ -3,6 +3,7 @@ import Mathlib.Data.Finset.Density import Mathlib.Data.Fintype.Order import Mathlib.Probability.ConditionalProbability import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup +import LeanAPAP.Prereqs.Expect.Basic import LeanAPAP.Prereqs.Expect.Complex import LeanAPAP.Prereqs.Expect.Order import LeanAPAP.Prereqs.Function.Translate diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean index dda2b05ffb..15bba63610 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean @@ -212,8 +212,6 @@ lemma norm_le_dLinftyNorm {i : α} : ‖f i‖ ≤ ‖f‖_[∞] := by @[simp] lemma dLpNorm_pos (hp : p ≠ 0) : 0 < ‖f‖_[p] ↔ f ≠ 0 := pos_iff_ne_zero.trans (dLpNorm_eq_zero hp).not -@[gcongr] lemma dLpNorm_mono_right (hpq : p ≤ q) : ‖f‖_[p] ≤ ‖f‖_[q] := sorry - lemma dLpNorm_mono_real {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : ‖f‖_[p] ≤ ‖g‖_[p] := nnLpNorm_mono_real .of_discrete h diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index 651afa53ab..8f80578f18 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -30,7 +30,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι) _ = |(∑ b in B, ∑ i, (f (a i) - f (b i))) / B.card| ^ (m + 1) := by simp only [sum_sub_distrib] 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₀] + Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀] positivity _ = |∑ b in B, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / B.card ^ (m + 1) := by rw [abs_div, div_pow, Nat.abs_cast] @@ -174,7 +174,7 @@ private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) : 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_piFinset, prod_const, - card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀] + Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀] norm_num positivity diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index d42b1b9348..efde1e2939 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/LeanAPAP/Prereqs/NNLpNorm.lean @@ -1,9 +1,9 @@ +import Mathlib.Algebra.BigOperators.Expect import Mathlib.Analysis.Normed.Group.Constructions import Mathlib.MeasureTheory.Integral.Bochner import Mathlib.Tactic.Positivity.Finset import LeanAPAP.Mathlib.Algebra.Order.Module.Rat import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic -import LeanAPAP.Prereqs.Expect.Basic open Filter open scoped BigOperators ComplexConjugate ENNReal NNReal diff --git a/LeanAPAP/Prereqs/PointwiseDensity.lean b/LeanAPAP/Prereqs/PointwiseDensity.lean index aabc07d1ff..dca272e63f 100644 --- a/LeanAPAP/Prereqs/PointwiseDensity.lean +++ b/LeanAPAP/Prereqs/PointwiseDensity.lean @@ -1,5 +1,5 @@ +import Mathlib.Algebra.Group.Pointwise.Finset.Basic import Mathlib.Data.Finset.Density -import Mathlib.Data.Finset.Pointwise.Basic open scoped Pointwise diff --git a/lake-manifest.json b/lake-manifest.json index d4ca8068f8..d556b65b24 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85", + "rev": "2ce0037d487217469a1efeb9ea8196fe15ab9c46", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e5e4f1e9385f5a636cd95f7b5833d9ba7907115c", + "rev": "61fb4d1a2a6a4fe4be260ca31c58af1234ff298b", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -61,11 +61,21 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "4b83244f3ea8cf1ebc70f68bc5b94691e826c827", + "rev": "555be78e7f1df5d448c64e4282ece0dcc21214ff", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,