From 1aa59db87d58106b60b53cda45805ef54b70ee59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 29 Oct 2024 23:39:13 +0000 Subject: [PATCH] Clean up immediately upstreamable prerequisites --- PFR.lean | 9 +++- PFR/ApproxHomPFR.lean | 54 ++++++++----------- PFR/Endgame.lean | 8 +-- PFR/ForMathlib/AffineSpaceDim.lean | 45 ++++++++++------ PFR/ForMathlib/Entropy/Basic.lean | 8 +-- PFR/ForMathlib/Entropy/Kernel/Basic.lean | 9 ++-- PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean | 2 +- PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean | 4 +- PFR/ForMathlib/Entropy/RuzsaDist.lean | 19 ++++--- PFR/ForMathlib/FiniteRange/Defs.lean | 19 ++----- PFR/ForMathlib/GroupQuot.lean | 7 +-- PFR/ForMathlib/ZModModule.lean | 37 ++----------- PFR/ImprovedPFR.lean | 6 +-- PFR/Kullback.lean | 6 --- PFR/Main.lean | 2 +- PFR/Mathlib/Algebra/AddTorsor.lean | 11 ++++ PFR/Mathlib/Algebra/Group/Prod.lean | 18 +++++++ PFR/Mathlib/Algebra/Module/ZMod.lean | 8 +++ PFR/Mathlib/Data/Set/Pointwise/Finite.lean | 41 -------------- PFR/Mathlib/GroupTheory/PGroup.lean | 10 ++++ .../AffineSpace/AffineSubspace.lean | 13 +++++ .../LinearAlgebra/Dimension/Finrank.lean | 4 ++ .../MeasureTheory/Integral/Bochner.lean | 14 ----- .../MeasureTheory/Integral/IntegrableOn.lean | 11 ++++ .../MeasureTheory/Integral/SetIntegral.lean | 9 +--- PFR/WeakPFR.lean | 53 +++++++++--------- 26 files changed, 202 insertions(+), 225 deletions(-) create mode 100644 PFR/Mathlib/Algebra/AddTorsor.lean create mode 100644 PFR/Mathlib/Algebra/Group/Prod.lean create mode 100644 PFR/Mathlib/Algebra/Module/ZMod.lean delete mode 100644 PFR/Mathlib/Data/Set/Pointwise/Finite.lean create mode 100644 PFR/Mathlib/GroupTheory/PGroup.lean create mode 100644 PFR/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean create mode 100644 PFR/Mathlib/LinearAlgebra/Dimension/Finrank.lean delete mode 100644 PFR/Mathlib/MeasureTheory/Integral/Bochner.lean create mode 100644 PFR/Mathlib/MeasureTheory/Integral/IntegrableOn.lean diff --git a/PFR.lean b/PFR.lean index a92c51ba..183776b6 100644 --- a/PFR.lean +++ b/PFR.lean @@ -31,13 +31,18 @@ import PFR.HundredPercent import PFR.ImprovedPFR import PFR.Kullback import PFR.Main +import PFR.Mathlib.Algebra.AddTorsor import PFR.Mathlib.Algebra.Group.Pointwise.Set.Basic +import PFR.Mathlib.Algebra.Group.Prod +import PFR.Mathlib.Algebra.Module.ZMod import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog -import PFR.Mathlib.Data.Set.Pointwise.Finite import PFR.Mathlib.Data.Set.Pointwise.SMul +import PFR.Mathlib.GroupTheory.PGroup +import PFR.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace +import PFR.Mathlib.LinearAlgebra.Dimension.Finrank import PFR.Mathlib.MeasureTheory.Constructions.Pi -import PFR.Mathlib.MeasureTheory.Integral.Bochner +import PFR.Mathlib.MeasureTheory.Integral.IntegrableOn import PFR.Mathlib.MeasureTheory.Integral.Lebesgue import PFR.Mathlib.MeasureTheory.Integral.SetIntegral import PFR.Mathlib.MeasureTheory.Measure.NullMeasurable diff --git a/PFR/ApproxHomPFR.lean b/PFR/ApproxHomPFR.lean index a3e25d2a..d84677d7 100644 --- a/PFR/ApproxHomPFR.lean +++ b/PFR/ApproxHomPFR.lean @@ -2,7 +2,7 @@ import Mathlib.Combinatorics.Additive.Energy import Mathlib.Analysis.Normed.Lp.PiLp import Mathlib.Analysis.InnerProductSpace.PiL2 import LeanAPAP.Extras.BSG -import PFR.Mathlib.Data.Set.Pointwise.Finite +import PFR.Mathlib.Algebra.Group.Prod import PFR.HomPFR /-! @@ -31,37 +31,31 @@ $|G|^2 / K$ pairs $(x,y) \in G^2$ such that $$ f(x+y) = f(x) + f(y).$$ Then there exists a homomorphism $\phi : G \to G'$ and a constant $c \in G'$ such that $f(x) = \phi(x)+c$ for at least $|G| / (2 ^ {172} * K ^ {146})$ values of $x \in G$. -/ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0) - (hf : Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2} ≥ Nat.card G ^ 2 / K) : + (hf : Nat.card G ^ 2 / K ≤ Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2}) : ∃ (φ : G →+ G') (c : G'), Nat.card {x | f x = φ x + c} ≥ Nat.card G / (2 ^ 172 * K ^ 146) := by let A := (Set.univ.graphOn f).toFinite.toFinset - - have h_cs : ((A ×ˢ A).filter (fun (a, a') ↦ a + a' ∈ A) |>.card : ℝ) ^ 2 ≤ - Finset.card A * E[A] := by - norm_cast - convert card_sq_le_card_mul_addEnergy A A A - rewrite [← Nat.card_eq_finsetCard, ← Nat.card_eq_finsetCard, - Nat.card_congr (Set.equivFilterGraph f)] at h_cs - - have hA : Nat.card A = Nat.card G := by - rw [← Nat.card_univ (α := G), ← Set.card_graphOn _ f, Nat.card_eq_finsetCard, - Set.Finite.card_toFinset] - simp - have hA_pos : 0 < (Nat.card A : ℝ) := Nat.cast_pos.mpr <| Nat.card_pos.trans_eq hA.symm - have : (Nat.card G ^2 / K)^2 ≤ Nat.card A * E[A] := LE.le.trans (by gcongr) h_cs - rewrite [← hA] at this - replace : E[A] ≥ (Finset.card A)^3 / K^2 := calc - _ ≥ (Nat.card A ^ 2 / K)^2 / Nat.card A := (div_le_iff₀' <| hA_pos).mpr this - _ = (Nat.card A ^ 4 / Nat.card A) / K^2 := by ring - _ = A.card ^ 3 / K ^ 2 := by - rw [pow_succ, mul_div_assoc, div_self (ne_of_gt hA_pos), mul_one, - Nat.card_eq_finsetCard] + have hA : #A = Nat.card G := by rw [Set.Finite.card_toFinset]; simp [← Nat.card_eq_fintype_card] have hA_nonempty : A.Nonempty := by simp [-Set.Finite.toFinset_setOf, A] + have hA_pos : 0 < #A := by positivity + have := calc + (#A ^ 3 / K ^ 2 : ℝ) + = (Nat.card G ^ 2 / K) ^ 2 / #A := by field_simp [hA]; ring + _ ≤ Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2} ^ 2 / #A := by gcongr + _ = #{ab ∈ A ×ˢ A | ab.1 + ab.2 ∈ A} ^ 2 / #A := by + congr + rw [← Nat.card_eq_finsetCard, ← Finset.coe_sort_coe, Finset.coe_filter, + Set.Finite.toFinset_prod] + simp only [Set.Finite.mem_toFinset, A] + rw [Nat.card_congr (addMemGraphEquiv ..)] + simp + _ ≤ #A * E[A] / #A := by gcongr; exact mod_cast card_sq_le_card_mul_addEnergy .. + _ = E[A] := by field_simp obtain ⟨A', hA', hA'1, hA'2⟩ := BSG_self' (sq_nonneg K) hA_nonempty (by simpa only [inv_mul_eq_div] using this) - clear h_cs hf this + clear hf this have hA'₀ : A'.Nonempty := Finset.card_pos.1 $ Nat.cast_pos.1 $ hA'1.trans_lt' $ by positivity let A'' := A'.toSet - have hA''_coe : Nat.card A'' = Finset.card A' := Nat.card_eq_finsetCard A' + have hA''_coe : Nat.card A'' = #A' := Nat.card_eq_finsetCard A' have hA''_pos : 0 < Nat.card A'' := by rw [hA''_coe]; exact hA'₀.card_pos have hA''_nonempty : Set.Nonempty A'' := nonempty_subtype.mp (Finite.card_pos_iff.mp hA''_pos) have : Finset.card (A' - A') = Nat.card (A'' + A'') := calc @@ -146,7 +140,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0) · obtain ⟨ch, hch⟩ := Finset.mem_biUnion.mp hx exact ((Set.Finite.mem_toFinset _).mp hch.2).1 - replace : ∑ __ in cH₁, ((2 ^ 4)⁻¹ * (K ^ 2)⁻¹ * A.card / cH₁.card : ℝ) ≤ + replace : ∑ __ in cH₁, ((2 ^ 4)⁻¹ * (K ^ 2)⁻¹ * #A / cH₁.card : ℝ) ≤ ∑ ch in cH₁, ((translate ch.1 ch.2).toFinite.toFinset.card : ℝ) := by rewrite [Finset.sum_const, nsmul_eq_mul, ← mul_div_assoc, mul_div_right_comm, div_self, one_mul] · apply hA'1.trans @@ -155,7 +149,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0) · symm refine ne_of_lt <| Nat.cast_zero.symm.trans_lt <| Nat.cast_lt.mpr <| Finset.card_pos.mpr ?_ exact (Set.Finite.toFinset_nonempty _).mpr h_nonempty - replace : ∃ c' : G × G', ∃ h : G', (2 ^ 4 : ℝ)⁻¹ * (K ^ 2)⁻¹ * A.card / cH₁.card ≤ + replace : ∃ c' : G × G', ∃ h : G', (2 ^ 4 : ℝ)⁻¹ * (K ^ 2)⁻¹ * #A / cH₁.card ≤ Nat.card { x : G | f x = φ x + (-φ c'.1 + c'.2 + h) } := by obtain ⟨ch, hch⟩ := Finset.exists_le_of_sum_le ((Set.Finite.toFinset_nonempty _).mpr h_nonempty) this @@ -168,12 +162,10 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0) use φ, -φ c'.1 + c'.2 + h refine le_trans ?_ hch unfold_let cH₁ - rewrite [← Nat.card_eq_finsetCard, hA, ← mul_inv, inv_mul_eq_div, div_div] + rewrite [hA, ← mul_inv, inv_mul_eq_div, div_div] apply div_le_div (Nat.cast_nonneg _) le_rfl · apply mul_pos - · apply mul_pos - · norm_num - · exact sq_pos_of_pos hK + · positivity · rewrite [Nat.cast_pos, Finset.card_pos, Set.Finite.toFinset_nonempty _] exact h_nonempty rw [show 146 = 2 + 144 by norm_num, show 172 = 4 + 168 by norm_num, pow_add, pow_add, diff --git a/PFR/Endgame.lean b/PFR/Endgame.lean index 694f50e6..28a7c77a 100644 --- a/PFR/Endgame.lean +++ b/PFR/Endgame.lean @@ -393,7 +393,7 @@ lemma construct_good_prelim : simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum2] simp_rw [condRuzsaDist'_eq_sum hT₁ hT₃, - integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum, + integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset, Measure.map_apply hT₃ (.singleton _), smul_eq_mul] gcongr @@ -404,7 +404,7 @@ lemma construct_good_prelim : simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum3] simp_rw [condRuzsaDist'_eq_sum hT₂ hT₃, - integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum, + integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset, Measure.map_apply hT₃ (.singleton _), smul_eq_mul] gcongr linarith [condRuzsaDist_le' ℙ ℙ p.hmeas2 hT₂ hT₃] @@ -458,7 +458,7 @@ local notation3:max "δ'" => I[T₁ : T₂|R] + I[T₂ : T₃|R] + I[T₃ : T₁ omit [AddCommGroup G] in lemma delta'_eq_integral : δ' = (Measure.map R ℙ)[fun r => δ[ℙ[|R⁻¹' {r}]]] := by - simp_rw [condMutualInfo_eq_integral_mutualInfo, integral_eq_sum, smul_add, + simp_rw [condMutualInfo_eq_integral_mutualInfo, integral_fintype _ .of_finite, smul_add, Finset.sum_add_distrib] include hT₁ hT₂ hT₃ hT h_min hR hX₁ hX₂ in @@ -474,7 +474,7 @@ lemma cond_construct_good [IsProbabilityMeasure (ℙ : Measure Ω)] : k = (Measure.map R ℙ)[fun _r => k] := by rw [integral_const]; simp _ ≤ _ := ?_ - simp_rw [integral_eq_sum] + simp_rw [integral_fintype _ .of_finite] apply Finset.sum_le_sum intro r _ by_cases hr : ℙ (R⁻¹' {r}) = 0 diff --git a/PFR/ForMathlib/AffineSpaceDim.lean b/PFR/ForMathlib/AffineSpaceDim.lean index dac03960..05b89511 100644 --- a/PFR/ForMathlib/AffineSpaceDim.lean +++ b/PFR/ForMathlib/AffineSpaceDim.lean @@ -1,23 +1,36 @@ -import Mathlib.LinearAlgebra.Dimension.Finrank -import Mathlib.RingTheory.Finiteness +import Mathlib.LinearAlgebra.Dimension.Constructions +import Mathlib.LinearAlgebra.Dimension.Finite +import PFR.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace +import PFR.Mathlib.LinearAlgebra.Dimension.Finrank -variable {G : Type*} [AddCommGroup G] +open scoped Pointwise -/-- If G ≅ ℤᵈ then there is a subgroup H of G such that A lies in a coset of H. This is helpful to -give the equivalent definition of `dimension`. Here this is stated in greated generality since the -proof carries over automatically. -/ -lemma exists_coset_cover (A : Set G) : - ∃ (d : ℕ), ∃ (S : Submodule ℤ G) (v : G), Module.finrank ℤ S = d ∧ ∀ a ∈ A, a - v ∈ S := - ⟨Module.finrank ℤ (⊤ : Submodule ℤ G), ⊤, by simp⟩ +namespace AffineSpace +variable {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} + {S : Submodule k V} --- TODO: Redefine as `Module.finrank ℤ (vectorSpan ℤ A)` +variable (k) in open scoped Classical in /-- The dimension of the affine span over `ℤ` of a subset of an additive group. -/ -noncomputable def dimension (A : Set G) : ℕ := Nat.find (exists_coset_cover A) +noncomputable def finrank (s : Set P) : ℕ := (vectorSpan k s).finrank -lemma dimension_le_of_coset_cover (A : Set G) (S : Submodule ℤ G) (v : G) - (hA : ∀ a ∈ A, a - v ∈ S) : dimension A ≤ Module.finrank ℤ S := by - classical exact Nat.find_le ⟨S , v, rfl, hA⟩ +variable (k) in +@[simp] +lemma finrank_vadd_set (s : Set P) (v : V) : finrank k (v +ᵥ s) = AffineSpace.finrank k s := by + simp [finrank] -lemma dimension_le_rank [Module.Finite ℤ G] (A : Set G) : dimension A ≤ Module.finrank ℤ G := by - simpa using dimension_le_of_coset_cover A ⊤ 0 (by simp) +variable (k) in +@[simp] lemma finrank_empty [Nontrivial k] : finrank k (∅ : Set P) = 0 := by simp [finrank] + +variable [StrongRankCondition k] + +lemma finrank_le_submoduleFinrank [Module.Finite k S] (q : P) (hs : ∀ p ∈ s, p -ᵥ q ∈ S) : + finrank k s ≤ S.finrank := by + refine Submodule.finrank_mono ?_ + simpa [vectorSpan, Submodule.span_le, Set.vsub_subset_iff] + using fun a ha b hb ↦ S.sub_mem (hs _ ha) (hs _ hb) + +lemma finrank_le_moduleFinrank [Module.Finite k V] : finrank k s ≤ Module.finrank k V := + (vectorSpan k s).finrank_le + +end AffineSpace diff --git a/PFR/ForMathlib/Entropy/Basic.lean b/PFR/ForMathlib/Entropy/Basic.lean index a74c6412..3955c2ab 100644 --- a/PFR/ForMathlib/Entropy/Basic.lean +++ b/PFR/ForMathlib/Entropy/Basic.lean @@ -446,7 +446,7 @@ lemma condEntropy_le_log_card [MeasurableSingletonClass S] [Fintype S] lemma condEntropy_eq_sum [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω) [IsFiniteMeasure μ] (hY : Measurable Y) [FiniteRange Y]: H[X | Y ; μ] = ∑ y in FiniteRange.toFinset Y, (μ.map Y {y}).toReal * H[X | Y ← y ; μ] := by - rw [condEntropy_def, integral_eq_setIntegral (full_measure_of_finiteRange hY), setIntegral_eq_sum] + rw [condEntropy_def, integral_eq_setIntegral (full_measure_of_finiteRange hY), integral_finset _ _ IntegrableOn.finset] simp_rw [smul_eq_mul] /-- `H[X|Y] = ∑_y P[Y=y] H[X|Y=y]`$.-/ @@ -454,7 +454,7 @@ lemma condEntropy_eq_sum_fintype [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω) [IsFiniteMeasure μ] (hY : Measurable Y) [Fintype T] : H[X | Y ; μ] = ∑ y, (μ (Y ⁻¹' {y})).toReal * H[X | Y ← y ; μ] := by - rw [condEntropy_def, integral_eq_sum] + rw [condEntropy_def, integral_fintype _ .of_finite] simp_rw [smul_eq_mul, Measure.map_apply hY (.singleton _)] variable [MeasurableSingletonClass T] @@ -828,7 +828,7 @@ lemma condMutualInfo_eq_kernel_mutualInfo I[X : Y | Z ; μ] = Ik[condDistrib (⟨X, Y⟩) Z μ, μ.map Z] := by rcases finiteSupport_of_finiteRange (μ := μ) (X := Z) with ⟨A, hA⟩ simp_rw [condMutualInfo_def, entropy_def, Kernel.mutualInfo, Kernel.entropy, - integral_eq_setIntegral hA, setIntegral_eq_sum, smul_eq_mul, mul_sub, mul_add, + integral_eq_setIntegral hA, integral_finset _ _ IntegrableOn.finset, smul_eq_mul, mul_sub, mul_add, Finset.sum_sub_distrib, Finset.sum_add_distrib] congr with x · have h := condDistrib_fst_ae_eq hX hY hZ μ @@ -857,7 +857,7 @@ lemma condMutualInfo_eq_sum [MeasurableSingletonClass U] [IsFiniteMeasure μ] I[X : Y | Z ; μ] = ∑ z in FiniteRange.toFinset Z, (μ (Z ⁻¹' {z})).toReal * I[X : Y ; (μ[|Z ← z])] := by rw [condMutualInfo_eq_integral_mutualInfo, - integral_eq_setIntegral (FiniteRange.null_of_compl _ Z), setIntegral_eq_sum] + integral_eq_setIntegral (FiniteRange.null_of_compl _ Z), integral_finset _ _ IntegrableOn.finset] congr 1 with z rw [map_apply hZ (MeasurableSet.singleton z)] rfl diff --git a/PFR/ForMathlib/Entropy/Kernel/Basic.lean b/PFR/ForMathlib/Entropy/Kernel/Basic.lean index a1ba9ad3..0c104fdd 100644 --- a/PFR/ForMathlib/Entropy/Kernel/Basic.lean +++ b/PFR/ForMathlib/Entropy/Kernel/Basic.lean @@ -1,6 +1,6 @@ import Mathlib.MeasureTheory.Integral.Prod import PFR.ForMathlib.Entropy.Measure -import PFR.Mathlib.MeasureTheory.Integral.Bochner +import PFR.Mathlib.MeasureTheory.Integral.IntegrableOn import PFR.Mathlib.MeasureTheory.Integral.SetIntegral import PFR.Mathlib.Probability.Kernel.Disintegration @@ -167,7 +167,8 @@ lemma entropy_comap [MeasurableSingletonClass T] exact MeasurableSet.compl (Finset.measurableSet A) exact ae_eq_univ.mp hf_range simp_rw [entropy] - simp_rw [integral_eq_setIntegral hA, integral_eq_setIntegral this, setIntegral_eq_sum, + simp_rw [integral_eq_setIntegral hA, integral_eq_setIntegral this, + integral_finset _ _ IntegrableOn.finset, Measure.comap_apply f hf.injective hf.measurableSet_image' _ (.singleton _)] simp only [Set.image_singleton, smul_eq_mul] simp_rw [comap_apply] @@ -223,7 +224,7 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas · simp let A := μ.support have hsum (F : T → ℝ) : ∫ (t : T), F t ∂μ = ∑ t in A, (μ.real {t}) * (F t) := by - rw [integral_eq_setIntegral (measure_compl_support μ), setIntegral_eq_sum] + rw [integral_eq_setIntegral (measure_compl_support μ), integral_finset _ _ IntegrableOn.finset] congr with t ht simp_rw [entropy, hsum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl @@ -246,7 +247,7 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas simp at hu ⊢ exact hu hs exact MeasurableSet.compl (Finset.measurableSet _) - rw [measureEntropy_def_finite' hκη, measureEntropy_def_finite' (hB t ht), setIntegral_eq_sum, + rw [measureEntropy_def_finite' hκη, measureEntropy_def_finite' (hB t ht), integral_finset _ _ IntegrableOn.finset, ← Finset.sum_add_distrib, Finset.sum_product] apply Finset.sum_congr rfl intro s hs diff --git a/PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean b/PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean index ff0af788..9a738e20 100644 --- a/PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean +++ b/PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean @@ -120,7 +120,7 @@ lemma mutualInfo_nonneg' {κ : Kernel T (S × U)} {μ : Measure T} [IsFiniteMeas [FiniteSupport μ] (hκ : FiniteKernelSupport κ) : 0 ≤ Ik[κ, μ] := by simp_rw [mutualInfo, entropy, integral_eq_setIntegral (measure_compl_support μ), - setIntegral_eq_sum, smul_eq_mul] + integral_finset _ _ IntegrableOn.finset, smul_eq_mul] rw [← Finset.sum_add_distrib, ← Finset.sum_sub_distrib] refine Finset.sum_nonneg (fun x _ ↦ ?_) by_cases hx : μ {x} = 0 diff --git a/PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean b/PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean index c503d58b..b0cfc377 100644 --- a/PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean +++ b/PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean @@ -295,7 +295,7 @@ lemma rdist_triangle_aux1 (κ : Kernel T G) (η : Kernel T' G) (((μ.support ×ˢ μ''.support) ×ˢ μ'.support : Finset ((T × T'') × T')) : Set ((T × T'') × T'))ᶜ = 0 := Measure.prod_of_full_measure_finset hAC (measure_compl_support μ') - simp_rw [entropy, integral_eq_setIntegral hAB, integral_eq_setIntegral hACB, setIntegral_eq_sum, + simp_rw [entropy, integral_eq_setIntegral hAB, integral_eq_setIntegral hACB, integral_finset _ _ IntegrableOn.finset, smul_eq_mul, Measure.prod_apply_singleton, Finset.sum_product, ENNReal.toReal_mul, mul_assoc, ← Finset.mul_sum] congr with x @@ -326,7 +326,7 @@ lemma rdist_triangle_aux2 (η : Kernel T' G) (ξ : Kernel T'' G) (((μ.support ×ˢ μ''.support) ×ˢ μ'.support : Finset ((T × T'') × T')) : Set ((T × T'') × T'))ᶜ = 0 := Measure.prod_of_full_measure_finset hAC (measure_compl_support μ') - simp_rw [entropy, integral_eq_setIntegral hACB, integral_eq_setIntegral hBC, setIntegral_eq_sum, + simp_rw [entropy, integral_eq_setIntegral hACB, integral_eq_setIntegral hBC, integral_finset _ _ IntegrableOn.finset, smul_eq_mul, Measure.prod_apply_singleton] conv_rhs => rw [Finset.sum_product_right] conv_lhs => rw [Finset.sum_product, Finset.sum_product_right] diff --git a/PFR/ForMathlib/Entropy/RuzsaDist.lean b/PFR/ForMathlib/Entropy/RuzsaDist.lean index 5ae8919f..261d635d 100644 --- a/PFR/ForMathlib/Entropy/RuzsaDist.lean +++ b/PFR/ForMathlib/Entropy/RuzsaDist.lean @@ -466,7 +466,7 @@ lemma condRuzsaDist_eq_sum' {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : d[X | Z ; μ # Y | W ; μ'] = ∑ z, ∑ w, (μ (Z ⁻¹' {z})).toReal * (μ' (W ⁻¹' {w})).toReal * d[X ; (μ[|Z ← z]) # Y ; (μ'[|W ← w])] := by - rw [condRuzsaDist_def, Kernel.rdist, integral_eq_sum] + rw [condRuzsaDist_def, Kernel.rdist, integral_fintype _ .of_finite] simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, smul_eq_mul, Fintype.sum_prod_type, Measure.map_apply hZ (.singleton _), Measure.map_apply hW (.singleton _)] @@ -502,7 +502,7 @@ lemma condRuzsaDist_eq_sum {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω simp [← FiniteRange.range] measurability } - rw [condRuzsaDist_def, Kernel.rdist, integral_eq_setIntegral this, setIntegral_eq_sum] + rw [condRuzsaDist_def, Kernel.rdist, integral_eq_setIntegral this, integral_finset _ _ IntegrableOn.finset] simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, smul_eq_mul, Finset.sum_product, Measure.map_apply hZ (.singleton _), Measure.map_apply hW (.singleton _)] @@ -583,7 +583,7 @@ lemma condRuzsaDist'_eq_sum {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} (hY : convert measure_empty (μ := μ) simp [← FiniteRange.range] measurability - rw [condRuzsaDist'_def, Kernel.rdist, integral_eq_setIntegral this, setIntegral_eq_sum] + rw [condRuzsaDist'_def, Kernel.rdist, integral_eq_setIntegral this, integral_finset _ _ IntegrableOn.finset] simp_rw [Measure.prod_apply_singleton, smul_eq_mul, Finset.sum_product] simp only [Finset.univ_unique, PUnit.default_eq_unit, MeasurableSpace.measurableSet_top, Measure.dirac_apply', Set.mem_singleton_iff, Set.indicator_of_mem, Pi.one_apply, one_mul, @@ -680,9 +680,8 @@ lemma condRuzsaDist'_eq_integral (X : Ω → G) {Y : Ω' → G} {W : Ω' → T} convert measure_empty (μ := μ) simp [← FiniteRange.range] measurability - rw [integral_eq_setIntegral this] - convert symm $ setIntegral_eq_sum (μ'.map W) _ (fun w ↦ d[X ; μ # Y ; (μ'[|W ← w])]) - rw [Measure.map_apply hW (MeasurableSet.singleton _)] + rw [integral_eq_setIntegral this, integral_finset _ _ IntegrableOn.finset] + simp [Measure.map_apply hW (MeasurableSet.singleton _)] section @@ -832,8 +831,8 @@ lemma condRuzsaDist_of_copy {X : Ω → G} (hX : Measurable X) {Z : Ω → S} (h measurability } rw [condRuzsaDist_def, condRuzsaDist_def, Kernel.rdist, Kernel.rdist, - integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', setIntegral_eq_sum, - setIntegral_eq_sum] + integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', integral_finset _ _ IntegrableOn.finset, + integral_finset _ _ IntegrableOn.finset] have hZZ' : μ.map Z = μ''.map Z' := (h1.comp measurable_snd).map_eq have hWW' : μ'.map W = μ'''.map W' := (h2.comp measurable_snd).map_eq simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, ← hZZ', ← hWW', @@ -904,8 +903,8 @@ lemma condRuzsaDist'_of_copy (X : Ω → G) {Y : Ω' → G} (hY : Measurable Y) simp [← FiniteRange.range] measurability rw [condRuzsaDist'_def, condRuzsaDist'_def, Kernel.rdist, Kernel.rdist, - integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', setIntegral_eq_sum, - setIntegral_eq_sum] + integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', integral_finset _ _ IntegrableOn.finset, + integral_finset _ _ IntegrableOn.finset] have hWW' : μ'.map W = μ'''.map W' := (h2.comp measurable_snd).map_eq simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, ← hWW', Measure.map_apply hW (.singleton _)] diff --git a/PFR/ForMathlib/FiniteRange/Defs.lean b/PFR/ForMathlib/FiniteRange/Defs.lean index 27b16372..7aa3e8b8 100644 --- a/PFR/ForMathlib/FiniteRange/Defs.lean +++ b/PFR/ForMathlib/FiniteRange/Defs.lean @@ -1,9 +1,4 @@ -import Mathlib.Data.Set.Image -import Mathlib.Data.Set.Finite -import Mathlib.Data.Fintype.Basic -import Mathlib.Algebra.Group.Defs import Mathlib.MeasureTheory.Measure.MeasureSpace -import PFR.ForMathlib.Pair /-- The property of having a finite range. -/ class FiniteRange {Ω G : Type*} (X : Ω → G) : Prop where @@ -62,20 +57,14 @@ instance {Ω Ω' G : Type*} (X : Ω → G) (f : Ω' → Ω) [hX : FiniteRange X] /-- If X, Y have finite range, then so does the pair ⟨X, Y⟩. -/ instance {Ω G H : Type*} (X : Ω → G) (Y : Ω → H) [hX : FiniteRange X] [hY : FiniteRange Y] : - FiniteRange (⟨X, Y⟩) where - finite := by - have : Set.range (⟨X, Y⟩) ⊆ (Set.range X) ×ˢ (Set.range Y) := by - intro ⟨x, y⟩ hz - simp only [Set.mem_range, Prod.mk.injEq, Set.mem_prod] at hz ⊢ - rcases hz with ⟨ω, hω⟩ - exact ⟨⟨ω, hω.1⟩, ω, hω.2⟩ - exact Set.Finite.subset (Set.Finite.prod hX.finite hY.finite) this + FiniteRange fun ω ↦ (X ω, Y ω) where + finite := (hX.finite.prod hY.finite).subset (Set.range_pair_subset ..) /-- The product of functions of finite range, has finite range. -/ @[to_additive "The sum of functions of finite range, has finite range."] instance FiniteRange.mul {Ω G : Type*} (X Y : Ω → G) [Mul G] [hX: FiniteRange X] [hY: FiniteRange Y] : FiniteRange (X * Y) := by - show FiniteRange ((fun p ↦ p.1 * p.2) ∘ ⟨X, Y⟩) + show FiniteRange ((fun p ↦ p.1 * p.2) ∘ fun ω ↦ (X ω, Y ω)) infer_instance /-- The product of functions of finite range, has finite range. -/ @@ -87,7 +76,7 @@ instance FiniteRange.mul' {Ω G : Type*} (X Y : Ω → G) [Mul G] [FiniteRange X @[to_additive "The difference of functions of finite range, has finite range."] instance FiniteRange.div {Ω G : Type*} (X Y : Ω → G) [Div G] [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange (X/Y) := by - show FiniteRange ((fun p ↦ p.1 / p.2) ∘ ⟨X, Y⟩) + show FiniteRange ((fun p ↦ p.1 / p.2) ∘ fun ω ↦ (X ω, Y ω)) infer_instance /-- The product of functions of finite range, has finite range. -/ diff --git a/PFR/ForMathlib/GroupQuot.lean b/PFR/ForMathlib/GroupQuot.lean index 69c9b8a4..dda781f5 100644 --- a/PFR/ForMathlib/GroupQuot.lean +++ b/PFR/ForMathlib/GroupQuot.lean @@ -1,5 +1,6 @@ +import Mathlib.Algebra.EuclideanDomain.Int import Mathlib.LinearAlgebra.Dimension.Free -import PFR.ForMathlib.ZModModule +import PFR.Mathlib.Algebra.Module.ZMod /-! If `G` is a rank `d` free `ℤ`-module, then `G/nG` is a finite group of cardinality `n ^ d`. @@ -12,7 +13,7 @@ variable {G : Type*} [AddCommGroup G] [Module.Free ℤ G] {n : ℕ} variable (G n) in abbrev modN : Type _ := G ⧸ LinearMap.range (LinearMap.lsmul ℤ G n) -instance : Module (ZMod n) (modN G n) := .quotient_group (by simp) +instance : Module (ZMod n) (modN G n) := QuotientAddGroup.instZModModule (by simp) variable [NeZero n] @@ -58,4 +59,4 @@ instance modN.instFinite : Finite (modN G n) := Module.finite_of_finite (ZMod n) variable (G n) @[simp] lemma card_modN : Nat.card (modN G n) = n ^ Module.finrank ℤ G := by simp [Nat.card_congr modNBasis.repr.toEquiv, Nat.card_eq_fintype_card, - ← Module.finrank_eq_card_chooseBasisIndex] + Module.finrank_eq_card_chooseBasisIndex] diff --git a/PFR/ForMathlib/ZModModule.lean b/PFR/ForMathlib/ZModModule.lean index 3b7d9c46..b77c9249 100644 --- a/PFR/ForMathlib/ZModModule.lean +++ b/PFR/ForMathlib/ZModModule.lean @@ -1,40 +1,11 @@ import Mathlib.Algebra.Module.ZMod -import Mathlib.Data.Finsupp.Fintype import Mathlib.GroupTheory.Sylow +import PFR.Mathlib.GroupTheory.PGroup open Function Set ZMod -namespace Module -variable {p n : ℕ} {G : Type*} [AddCommGroup G] - -abbrev quotient_group {H : AddSubgroup G} (hH : ∀ x, p • x ∈ H) : Module (ZMod p) (G ⧸ H) := - AddCommGroup.zmodModule (by simpa [QuotientAddGroup.forall_mk, ← QuotientAddGroup.mk_nsmul]) - -section general -variable [Module (ZMod n) G] - -lemma isPGroup_multiplicative : IsPGroup n (Multiplicative G) := by - simpa [IsPGroup, Multiplicative.forall] using - fun _ ↦ ⟨1, by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]⟩ - -variable (n) in -lemma exists_finsupp {A : Set G} {x : G} (hx : x ∈ Submodule.span ℤ A) : - ∃ μ : A →₀ ZMod n, (μ.sum fun a r ↦ (ZMod.cast r : ℤ) • (a : G)) = x := by - rcases mem_span_set.1 hx with ⟨w, hw, rfl⟩; clear hx - use (w.subtypeDomain A).mapRange (↑) Int.cast_zero - rw [Finsupp.sum_mapRange_index (by simp)] - set A' := w.support.preimage ((↑) : A → G) injOn_subtype_val - erw [Finsupp.sum_subtypeDomain_index hw - (h := fun (a : G) (r : ℤ) ↦ (ZMod.cast (r : ZMod n) : ℤ) • a)] - refine (Finsupp.sum_congr ?_).symm - intro g _ - generalize w g = r - obtain ⟨k, hk⟩ : ∃ k : ℤ, (ZMod.cast (r : ZMod n) : ℤ) = r + n * k := by - use -(r / n) - rw_mod_cast [ZMod.coe_intCast, Int.emod_def, sub_eq_add_neg, mul_neg] - simp [hk, add_smul, mul_smul, ZModModule.char_nsmul_eq_zero] - -end general +namespace ZModModule +variable {p : ℕ} {G : Type*} [AddCommGroup G] /-- In an elementary abelian $p$-group, every finite subgroup $H$ contains a further subgroup of cardinality between $k$ and $pk$, if $k \leq |H|$.-/ @@ -46,4 +17,4 @@ lemma exists_submodule_subset_card_le (hp : p.Prime) [Module (ZMod p) G] {k : isPGroup_multiplicative hk h'k exact ⟨AddSubgroup.toZModSubmodule _ (AddSubgroup.toSubgroup.symm H'm), H'mk, kH'm, H'mHm⟩ -end Module +end ZModModule diff --git a/PFR/ImprovedPFR.lean b/PFR/ImprovedPFR.lean index bbaf0c58..080426e6 100644 --- a/PFR/ImprovedPFR.lean +++ b/PFR/ImprovedPFR.lean @@ -349,14 +349,14 @@ lemma construct_good_prelim' : k ≤ δ + p.η * c[T₁ | T₃ # T₂ | T₃] := simp only [sum2, integral_sub .of_finite .of_finite, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj] simp_rw [condRuzsaDist'_eq_sum hT₁ hT₃, - integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum, + integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset, Measure.map_apply hT₃ (.singleton _), smul_eq_mul] have h3 : sum3 = d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂] := by simp only [sum3, integral_sub .of_finite .of_finite, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj] simp_rw [condRuzsaDist'_eq_sum hT₂ hT₃, - integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum, + integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset, Measure.map_apply hT₃ (.singleton _), smul_eq_mul] -- put all these estimates together to bound sum4 have h4 : sum4 ≤ δ + p.η * ((d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁]) @@ -1013,7 +1013,7 @@ theorem PFR_conjecture_improv (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K · obtain ⟨H', IH'A, IAH', H'H⟩ : ∃ H' : Submodule (ZMod 2) G, Nat.card H' ≤ Nat.card A ∧ Nat.card A < 2 * Nat.card H' ∧ H' ≤ H := by have A_pos' : 0 < Nat.card A := mod_cast A_pos - exact Module.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne' + exact ZModModule.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne' have : (Nat.card A / 2 : ℝ) < Nat.card H' := by rw [div_lt_iff₀ zero_lt_two, mul_comm]; norm_cast have H'_pos : (0 : ℝ) < Nat.card H' := by diff --git a/PFR/Kullback.lean b/PFR/Kullback.lean index 982f6be7..7e12aa1f 100644 --- a/PFR/Kullback.lean +++ b/PFR/Kullback.lean @@ -6,12 +6,6 @@ import PFR.ForMathlib.Entropy.Basic # Kullback-Leibler divergence Definition of Kullback-Leibler divergence and basic facts - -## Main definitions: - - -## Main results - -/ open MeasureTheory ProbabilityTheory Real diff --git a/PFR/Main.lean b/PFR/Main.lean index 3c4f290a..eb87ba24 100644 --- a/PFR/Main.lean +++ b/PFR/Main.lean @@ -302,7 +302,7 @@ theorem PFR_conjecture (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.c · obtain ⟨H', IH'A, IAH', H'H⟩ : ∃ H' : Submodule (ZMod 2) G, Nat.card H' ≤ Nat.card A ∧ Nat.card A < 2 * Nat.card H' ∧ H' ≤ H := by have A_pos' : 0 < Nat.card A := mod_cast A_pos - exact Module.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne' + exact ZModModule.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne' have : (Nat.card A / 2 : ℝ) < Nat.card H' := by rw [div_lt_iff₀ zero_lt_two, mul_comm]; norm_cast have H'_pos : (0 : ℝ) < Nat.card H' := by diff --git a/PFR/Mathlib/Algebra/AddTorsor.lean b/PFR/Mathlib/Algebra/AddTorsor.lean new file mode 100644 index 00000000..ec13e0be --- /dev/null +++ b/PFR/Mathlib/Algebra/AddTorsor.lean @@ -0,0 +1,11 @@ +import Mathlib.Algebra.AddTorsor + +open scoped Pointwise + +namespace Set +variable {G P : Type*} [AddCommGroup G] [AddTorsor G P] + +@[simp] lemma vadd_set_vsub_vadd_set (v : G) (s t : Set P) : (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t := by + ext; simp [mem_vsub, mem_vadd_set] + +end Set diff --git a/PFR/Mathlib/Algebra/Group/Prod.lean b/PFR/Mathlib/Algebra/Group/Prod.lean new file mode 100644 index 00000000..397ff44d --- /dev/null +++ b/PFR/Mathlib/Algebra/Group/Prod.lean @@ -0,0 +1,18 @@ +import Mathlib.Algebra.Group.Prod +import Mathlib.Data.Set.Function + +open Set + +variable {α β : Type*} [Group α] [Group β] + +/-- The pairs of points in the graph of `f` satisfying that their sum still belongs to the graph +correspond to the pairs `(x, y)` with `f (x + y) = f x + f y` (by considering the first +coordinates). -/ +@[to_additive] +def mulMemGraphEquiv (f : α → β) (s : Set α) : + {ab ∈ s.graphOn f ×ˢ s.graphOn f | ab.1 * ab.2 ∈ univ.graphOn f} ≃ + {ab ∈ s ×ˢ s | f (ab.1 * ab.2) = f ab.1 * f ab.2} where + toFun := fun ⟨((a, fa), (b, fb)), h⟩ ↦ ⟨(a, b), by aesop⟩ + invFun := fun ⟨(a, b), ha⟩ ↦ ⟨((a, f a), (b, f b)), by aesop⟩ + left_inv _ := by aesop + right_inv _ := rfl diff --git a/PFR/Mathlib/Algebra/Module/ZMod.lean b/PFR/Mathlib/Algebra/Module/ZMod.lean new file mode 100644 index 00000000..f6664f26 --- /dev/null +++ b/PFR/Mathlib/Algebra/Module/ZMod.lean @@ -0,0 +1,8 @@ +import Mathlib.Algebra.Module.ZMod + +/-- The quotient of an abelian group by a subgroup containing all multiples of `n` is a +`n`-torsion group. -/ +-- See note [reducible non-instances] +abbrev QuotientAddGroup.instZModModule {n : ℕ} {G : Type*} [AddCommGroup G] {H : AddSubgroup G} + (hH : ∀ x, n • x ∈ H) : Module (ZMod n) (G ⧸ H) := + AddCommGroup.zmodModule <| by simpa [QuotientAddGroup.forall_mk, ← QuotientAddGroup.mk_nsmul] diff --git a/PFR/Mathlib/Data/Set/Pointwise/Finite.lean b/PFR/Mathlib/Data/Set/Pointwise/Finite.lean deleted file mode 100644 index 8e2ca227..00000000 --- a/PFR/Mathlib/Data/Set/Pointwise/Finite.lean +++ /dev/null @@ -1,41 +0,0 @@ -import Mathlib.Data.Set.Pointwise.Finite - -open Function -open scoped Pointwise - -namespace Set -variable {α β γ : Type*} {f g : α → β} {x : α × β} - -variable {α β : Type*} [AddCommGroup α] [Fintype α] [AddCommGroup β] [Fintype β] [DecidableEq α] - [DecidableEq β] - -/-- The pairs of points in the graph of `f` satisyfing that their sum still belongs to the -graph correspond to the pairs `(x, y)` with `f (x + y) = f x + f y` (by considering the first -coordinates). -/ -def equivFilterGraph (f : α → β) : - let A := (univ.graphOn f).toFinite.toFinset - (A ×ˢ A).filter (fun (a, a') ↦ a + a' ∈ A) ≃ {x : α × α | f (x.1 + x.2) = f x.1 + f x.2} where - toFun := fun ⟨a, ha⟩ ↦ by - let A := (univ.graphOn f).toFinite.toFinset - use (a.1.1, a.2.1) - apply Finset.mem_filter.mp at ha - have h {a} (ha : a ∈ A) : f a.1 = a.2 := by simpa [A] using ha - show f (a.1.1 + a.2.1) = (f a.1.1) + (f a.2.1) - rw [h (Finset.mem_product.mp ha.1).1, h (Finset.mem_product.mp ha.1).2] - exact h ha.2 - invFun := fun ⟨a, ha⟩ ↦ by - use ((a.1, f a.1), (a.2, f a.2)) - refine Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨?_, ?_⟩, ?_⟩ - <;> apply (univ.graphOn f).toFinite.mem_toFinset.mpr - · exact ⟨a.1, by simp⟩ - · exact ⟨a.2, by simp⟩ - · exact mem_graphOn.mpr (by simpa) - left_inv := fun ⟨x, hx⟩ ↦ by - apply Subtype.ext - show ((x.1.1, f x.1.1), x.2.1, f x.2.1) = x - obtain ⟨hx1, hx2⟩ := Finset.mem_product.mp (Finset.mem_filter.mp hx).1 - rewrite [(univ.graphOn f).toFinite.mem_toFinset] at hx1 hx2 - rw [(mem_graphOn.mp hx1).2, (mem_graphOn.1 hx2).2] - right_inv := fun _ ↦ rfl - -end Set diff --git a/PFR/Mathlib/GroupTheory/PGroup.lean b/PFR/Mathlib/GroupTheory/PGroup.lean new file mode 100644 index 00000000..604325e4 --- /dev/null +++ b/PFR/Mathlib/GroupTheory/PGroup.lean @@ -0,0 +1,10 @@ +import Mathlib.GroupTheory.PGroup + +namespace ZModModule +variable {n : ℕ} {G : Type*} [AddCommGroup G] [Module (ZMod n) G] + +lemma isPGroup_multiplicative : IsPGroup n (Multiplicative G) := by + simpa [IsPGroup, Multiplicative.forall] using + fun _ ↦ ⟨1, by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]⟩ + +end ZModModule diff --git a/PFR/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean b/PFR/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean new file mode 100644 index 00000000..a93bfe69 --- /dev/null +++ b/PFR/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean @@ -0,0 +1,13 @@ +import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace +import PFR.Mathlib.Algebra.AddTorsor + +open scoped Pointwise + +namespace AffineSpace +variable {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} + {S : Submodule k V} + +@[simp] lemma vectorSpan_vadd (s : Set P) (v : V) : vectorSpan k (v +ᵥ s) = vectorSpan k s := by + simp [vectorSpan] + +end AffineSpace diff --git a/PFR/Mathlib/LinearAlgebra/Dimension/Finrank.lean b/PFR/Mathlib/LinearAlgebra/Dimension/Finrank.lean new file mode 100644 index 00000000..fd776043 --- /dev/null +++ b/PFR/Mathlib/LinearAlgebra/Dimension/Finrank.lean @@ -0,0 +1,4 @@ +import Mathlib.LinearAlgebra.Dimension.Finrank + +noncomputable abbrev Submodule.finrank {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] + (S : Submodule R M) : ℕ := Module.finrank R S diff --git a/PFR/Mathlib/MeasureTheory/Integral/Bochner.lean b/PFR/Mathlib/MeasureTheory/Integral/Bochner.lean deleted file mode 100644 index 35d04955..00000000 --- a/PFR/Mathlib/MeasureTheory/Integral/Bochner.lean +++ /dev/null @@ -1,14 +0,0 @@ -import Mathlib.MeasureTheory.Integral.Bochner - -open scoped ENNReal - -namespace MeasureTheory -variable {α E : Type*} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] - [CompleteSpace E] - --- TODO: Replace `integral_fintype`? -lemma integral_eq_sum (μ : Measure α) [IsFiniteMeasure μ] [MeasurableSingletonClass α] [Fintype α] - (f : α → E) : ∫ x, f x ∂μ = ∑ x, (μ {x}).toReal • f x := - integral_fintype _ .of_finite - -end MeasureTheory diff --git a/PFR/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/PFR/Mathlib/MeasureTheory/Integral/IntegrableOn.lean new file mode 100644 index 00000000..49949c72 --- /dev/null +++ b/PFR/Mathlib/MeasureTheory/Integral/IntegrableOn.lean @@ -0,0 +1,11 @@ +import Mathlib.MeasureTheory.Integral.IntegrableOn + +namespace MeasureTheory +variable {α E : Type*} [MeasurableSpace α] [NormedAddCommGroup E] [MeasurableSingletonClass α] + +lemma IntegrableOn.finset {μ : Measure α} [IsFiniteMeasure μ] {s : Finset α} {f : α → E} : + IntegrableOn f s μ := by + rw [← s.toSet.biUnion_of_singleton] + simp [integrableOn_finset_iUnion, measure_lt_top] + +end MeasureTheory diff --git a/PFR/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/PFR/Mathlib/MeasureTheory/Integral/SetIntegral.lean index 9dd76ddf..bf57dfbe 100644 --- a/PFR/Mathlib/MeasureTheory/Integral/SetIntegral.lean +++ b/PFR/Mathlib/MeasureTheory/Integral/SetIntegral.lean @@ -4,16 +4,9 @@ open scoped ENNReal namespace MeasureTheory variable {α E : Type*} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] + lemma integral_eq_setIntegral {μ : Measure α} {s : Set α} (hs : μ sᶜ = 0) (f : α → E) : ∫ x, f x ∂μ = ∫ x in s, f x ∂μ := by rw [← setIntegral_univ, ← setIntegral_congr_set]; rwa [ae_eq_univ] -variable [MeasurableSingletonClass α] [CompleteSpace E] - -lemma setIntegral_eq_sum (μ : Measure α) [IsFiniteMeasure μ] (s : Finset α) (f : α → E) : - ∫ x in s, f x ∂μ = ∑ x ∈ s, (μ {x}).toReal • f x := by - refine integral_finset _ _ $ IntegrableOn.integrable ?_ - observe : s = ⋃ x ∈ s, {x} - simp [this, integrableOn_finset_iUnion, measure_lt_top] - end MeasureTheory diff --git a/PFR/WeakPFR.lean b/PFR/WeakPFR.lean index bc40b001..c47e4689 100644 --- a/PFR/WeakPFR.lean +++ b/PFR/WeakPFR.lean @@ -815,31 +815,30 @@ lemma weak_PFR_asymm_prelim (A B : Set G) [A_fin : Finite A] [B_fin : Finite B] def WeakPFRAsymmConclusion (A B : Set G) : Prop := ∃ A' B' : Set G, A' ⊆ A ∧ B' ⊆ B ∧ A'.Nonempty ∧ B'.Nonempty ∧ log ((Nat.card A * Nat.card B) / (Nat.card A' * (Nat.card B'))) ≤ 34 * dᵤ[A # B] ∧ - max (dimension A') (dimension B') ≤ (40 / log 2) * dᵤ[A # B] + max (AffineSpace.finrank ℤ A') (AffineSpace.finrank ℤ B') ≤ (40 / log 2) * dᵤ[A # B] /-- The property of two sets A,B of a group G not being contained in cosets of the same proper subgroup -/ def not_in_coset {G : Type*} [AddCommGroup G] (A B : Set G) : Prop := AddSubgroup.closure ((A - A) ∪ (B - B)) = ⊤ -/-- In fact one has equality here, but this is tricker to prove and not needed for the argument. -/ -lemma dimension_of_shift {G : Type*} [AddCommGroup G] {H : AddSubgroup G} (A : Set H) (x : G) : - dimension ((fun a : H ↦ (a : G) + x) '' A) ≤ dimension A := by +/-- In fact one has equality here, but this is trickier to prove and not needed for the argument. -/ +lemma dimension_of_shift {G : Type*} [AddCommGroup G] [Module.Finite ℤ G] {H : AddSubgroup G} + (A : Set H) (x : G) : + AffineSpace.finrank ℤ ((fun a : H ↦ (a : G) + x) '' A) = AffineSpace.finrank ℤ A := by classical - rcases Nat.find_spec (exists_coset_cover A) with ⟨S, v, hrank, hshift⟩ - change Module.finrank ℤ S = dimension A at hrank - rw [← hrank] - convert dimension_le_of_coset_cover _ (Submodule.map H.subtype.toIntLinearMap S) (x+v) ?_ - · apply LinearEquiv.finrank_eq - exact Submodule.equivMapOfInjective _ (by simpa using Subtype.val_injective) _ - intro a ha - rw [Set.mem_image] at ha - obtain ⟨b, hb, hb'⟩ := ha - rw [Submodule.mem_map] - use b - v, hshift b hb - simp [← hb'] - abel - -omit [Module.Free ℤ G] [Module.Finite ℤ G] in + calc + _ = AffineSpace.finrank ℤ (x +ᵥ Subtype.val '' A) := by + simp [← image_vadd, image_image, add_comm] + _ = AffineSpace.finrank ℤ (Subtype.val '' A) := by rw [AffineSpace.finrank_vadd_set] + _ = ((vectorSpan ℤ A).map H.subtype.toIntLinearMap).finrank := by + simp [AffineSpace.finrank, vectorSpan, Submodule.map_span] + congr! 2 + symm + exact image_image2_distrib fun _ _ ↦ rfl + _ = AffineSpace.finrank ℤ A := + (Submodule.equivMapOfInjective _ Subtype.val_injective _).symm.finrank_eq + +omit [Module.Free ℤ G] in lemma conclusion_transfers {A B : Set G} (G': AddSubgroup G) (A' B' : Set (G' : Set G)) (hA : IsShift A A') (hB : IsShift B B') [Finite A'] [Finite B'] @@ -906,8 +905,8 @@ lemma conclusion_transfers {A B : Set G} · convert LE.le.trans _ hdim_ineq using 2 norm_cast apply max_le_max - · exact dimension_of_shift A'' x - · exact dimension_of_shift B'' y + · exact (dimension_of_shift A'' x).le + · exact (dimension_of_shift B'' y).le /-- If $A,B\subseteq \mathbb{Z}^d$ are finite non-empty sets then there exist non-empty $A'\subseteq A$ and $B'\subseteq B$ such that @@ -1029,7 +1028,7 @@ lemma weak_PFR_asymm (A B : Set G) [Finite A] [Finite B] (hA : A.Nonempty) (hB : convert le_trans ?_ hdim using 1 · field_simp simp only [Nat.cast_max, max_le_iff, Nat.cast_le] - exact ⟨dimension_le_rank A, dimension_le_rank B⟩ + exact ⟨AffineSpace.finrank_le_moduleFinrank, AffineSpace.finrank_le_moduleFinrank⟩ /-- If $A\subseteq \mathbb{Z}^d$ is a finite non-empty set with $d[U_A;U_A]\leq \log K$ then there exists a non-empty $A'\subseteq A$ such that $\lvert A'\rvert\geq K^{-17}\lvert A\rvert$ @@ -1037,11 +1036,11 @@ and $\dim A'\leq \frac{40}{\log 2} \log K$. -/ lemma weak_PFR {A : Set G} [Finite A] {K : ℝ} (hA : A.Nonempty) (hK : 0 < K) (hdist : dᵤ[A # A] ≤ log K) : ∃ A' : Set G, A' ⊆ A ∧ K^(-17 : ℝ) * Nat.card A ≤ Nat.card A' ∧ - dimension A' ≤ (40 / log 2) * log K := by + AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by rcases weak_PFR_asymm A A hA hA with ⟨A', A'', hA', hA'', hA'nonempty, hA''nonempty, hcard, hdim⟩ have : ∃ B : Set G, B ⊆ A ∧ Nat.card B ≥ Nat.card A' ∧ Nat.card B ≥ Nat.card A'' - ∧ dimension B ≤ max (dimension A') (dimension A'') := by + ∧ AffineSpace.finrank ℤ B ≤ max (AffineSpace.finrank ℤ A') (AffineSpace.finrank ℤ A'') := by rcases lt_or_ge (Nat.card A') (Nat.card A'') with h | h · exact ⟨A'', hA'', by linarith, by linarith, le_max_right _ _⟩ · exact ⟨A', hA', by linarith, by linarith, le_max_left _ _⟩ @@ -1080,8 +1079,8 @@ lemma weak_PFR {A : Set G} [Finite A] {K : ℝ} (hA : A.Nonempty) (hK : 0 < K) convert this using 2 convert zpow_neg K 17 using 1 norm_cast - calc (dimension B : ℝ) - _ ≤ (((max (dimension A') (dimension A'')) : ℕ) : ℝ) := by norm_cast + calc (AffineSpace.finrank ℤ B : ℝ) + _ ≤ (((max (AffineSpace.finrank ℤ A') (AffineSpace.finrank ℤ A'')) : ℕ) : ℝ) := by norm_cast _ ≤ (40 / log 2) * dᵤ[A # A] := hdim _ ≤ (40 / log 2) * log K := mul_le_mul_of_nonneg_left hdist (by positivity) @@ -1091,7 +1090,7 @@ and $\dim A' \leq \frac{40}{\log 2} \log K$.-/ theorem weak_PFR_int {A : Set G} [A_fin : Finite A] (hnA : A.Nonempty) {K : ℝ} (hK : 0 < K) (hA : Nat.card (A-A) ≤ K * Nat.card A) : ∃ A' : Set G, A' ⊆ A ∧ Nat.card A' ≥ K ^ (-17 : ℝ) * Nat.card A ∧ - dimension A' ≤ (40 / log 2) * log K := by + AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by apply weak_PFR hnA hK ((rdist_set_le A A hnA hnA).trans _) suffices log (Nat.card (A-A)) ≤ log K + log (Nat.card A) by linarith rw [← log_mul (by positivity) _]