refactor multiRefPackage

PFR/BoundingMutual.lean

@@ -12,6 +12,7 @@ import PFR.MultiTauFunctional
 
 -/
 
+universe u
 open MeasureTheory ProbabilityTheory BigOperators
 
 -- Spelling here is *very* janky.  Feel free to respell
@@ -24,11 +25,8 @@ $$    {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m}
  $$
  Then ${\mathcal I} \leq 4 m^2 \eta k.$
 -/
-lemma mutual_information_le  (p : multiRefPackage) (Ω : Type*) [hΩ: MeasureSpace Ω] (X : ∀ i, Ω → p.G) (hindep:
-  iIndepFun (fun _ ↦ p.hGm) X)
-  (hmin : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω'] (X': Fin p.m × Fin p.m → Ω' → p.G) (hindep': iIndepFun (fun _ ↦ p.hGm) X') (hperm:
-  have _ := p.hGm
+lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Type u) [hΩ: MeasureSpace Ω] (X : ∀ i, Ω → G) (hindep:
+  iIndepFun (fun _ ↦ by infer_instance) X)
+  (hmin : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω'] (X': Fin p.m × Fin p.m → Ω' → G) (hindep': iIndepFun (fun _ ↦ by infer_instance) X') (hperm:
   ∀ j, ∃ e : Fin p.m ≃ Fin p.m, IdentDistrib (fun ω ↦ (fun i ↦ X' (i, j) ω) ) (fun ω ↦ (fun i ↦ X (e i) ω))) :
-  have _ := p.hG
-  have _ := p.hGm
   I[ fun ω ↦ ( fun j ↦ ∑ i, X' (i, j) ω) : fun ω ↦ ( fun i ↦ ∑ j, X' (i, j) ω) | fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ 4 * p.m^2 * p.η * D[ X; (fun _ ↦ hΩ)] := sorry

PFR/MultiTauFunctional.lean

@@ -13,52 +13,46 @@ Definition of the tau functional and basic facts
 -/
 
 open MeasureTheory ProbabilityTheory
-universe uG
-
-/-- A structure that packages all the fixed information in the main argument.  -/
-structure multiRefPackage :=
-  G : Type uG
-  hG : AddCommGroup G
-  hGf : Fintype G
-  hGm : MeasurableSpace G
-  hGsc : MeasurableSingletonClass G
-  m : ℕ
-  htorsion : ∀ x : G, m • x = 0
-  Ω₀ : Type*
-  hΩ₀ : MeasureSpace Ω₀
-  hprob : IsProbabilityMeasure (ℙ : Measure Ω₀)
-  X₀ : Ω₀ → G
-  hmeas : Measurable X₀
-  η : ℝ
-  hη : 0 < η
-
--- May need a lemma here that  [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] follows automatically from the given data
+universe u
+
+/-- We will frequently be working with finite additive groups with the discrete sigma-algebra. -/
+class MeasureableFinGroup (G : Type*)
+extends AddCommGroup G, Fintype G,
+          MeasurableSpace G, MeasurableSingletonClass G
+
+-- May need an instance lemma here that  [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] follows automatically from [MeasurableFinGroup G]
+
+/-- A structure that packages all the fixed information in the main argument.  See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Problem.20when.20instances.20are.20inside.20a.20structure for more discussion of the design choices here. -/
+structure multiRefPackage (G Ωₒ : Type*) [MeasureableFinGroup G] [MeasureSpace Ωₒ] where
+  (m : ℕ)
+  (hm : m ≥ 2)
+  (htorsion : ∀ x : G, m • x = 0)
+  (hprob : IsProbabilityMeasure (ℙ : Measure Ωₒ))
+  (X₀ : Ωₒ → G)
+  (hmeas : Measurable X₀)
+  (η : ℝ)
+  (hη : 0 < η)
+
 
 open BigOperators
 
--- Making the instances inside the multiRefPackage explicit is a hack.  Is there a more elegant way to do this?
 /-- If $(X_i)_{1 \leq i \leq m}$ is a tuple, we define its $\tau$-functional
 $$ \tau[ (X_i)_{1 \leq i \leq m}] := D[(X_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X_i; X^0].$$
 -/
-noncomputable def multiTau (p : multiRefPackage) (Ω : Fin p.m → Type*) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → p.G) : ℝ :=
-  let _ := p.hΩ₀
-  let _ := p.hG
-  let _ := p.hGm
+noncomputable def multiTau {G Ωₒ : Type*} [MeasureableFinGroup G] [MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type*) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G) : ℝ :=
   D[X; hΩ] + p.η * ∑ i, d[ X i # p.X₀ ]
 
 -- I can't figure out how to make a τ notation due to the dependent types in the arguments.  But perhaps we don't need one.  Also it may be better to define multiTau in terms of probability measures on G, rather than G-valued random variables, again to avoid dependent type issues.
 
+-- had to force objects to lie in a fixed universe `u` here to avoid a compilation error
 /-- A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional among all tuples of $G$-valued random variables. -/
-def multiTauMinimizes (p : multiRefPackage) (Ω : Fin p.m → Type*) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → p.G) : Prop := ∀ (Ω' : Fin p.m → Type*) (hΩ' : ∀ i, MeasureSpace (Ω' i)) (X': ∀ i, Ω' i → p.G), multiTau p Ω hΩ X ≤ multiTau p Ω' hΩ' X'
+def multiTauMinimizes {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G) : Prop := ∀ (Ω' : Fin p.m → Type u) (hΩ' : ∀ i, MeasureSpace (Ω' i)) (X': ∀ i, Ω' i → G), multiTau p Ω hΩ X ≤ multiTau p Ω' hΩ' X'
 
 /-- If $G$ is finite, then a $\tau$-minimizer exists. -/
-lemma multiTau_min_exists (p : multiRefPackage) : ∃ (Ω : Fin p.m → Type*) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → p.G), multiTauMinimizes p Ω hΩ X := by sorry
+lemma multiTau_min_exists {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) : ∃ (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G), multiTauMinimizes p Ω hΩ X := by sorry
 
 /-- If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, then $\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]$. -/
-lemma multiTau_min_sum_le (p : multiRefPackage) (Ω : Fin p.m → Type*) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → p.G) (hmin : multiTauMinimizes p Ω hΩ X):
-  let _ := p.hΩ₀
-  let _ := p.hG
-  let _ := p.hGm
+lemma multiTau_min_sum_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G) (hmin : multiTauMinimizes p Ω hΩ X):
   ∑ i, d[X i # p.X₀] ≤ 2 * p.m * p.η⁻¹ * d[p.X₀ # p.X₀] := by sorry
 
 /-- If  $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, and $k := D[(X_i)_{1 \leq i \leq m}]$, then for any other tuple $(X'_i)_{1 \leq i \leq m}$, one has

PFR/TorsionEndgame.lean

@@ -14,13 +14,15 @@ import PFR.BoundingMutual
 
 open MeasureTheory ProbabilityTheory BigOperators
 
-variable (p: multiRefPackage) (Ω : Fin p.m → Type*) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → p.G) (hmin : multiTauMinimizes p Ω hΩ X)
+section AnalyzeMinimizer
+
+universe u
+
+variable {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (X : ∀ i, Ω i → G) (hmin : multiTauMinimizes p Ω hΩ X)
 
 local notation3 "k" => multiTau p Ω hΩ X
 
-variable (Ω': Type*) [hΩ': MeasureSpace Ω'] (Y: Fin p.m × Fin p.m → Ω' → p.G) [IsFiniteMeasure hΩ'.volume] (hindep: iIndepFun (fun _ ↦ p.hGm) Y) (hident:
-  let _ := p.hGm
-  ∀ i, ∀ j, IdentDistrib (Y (i,j)) (X i) )
+variable (Ω': Type u) [hΩ': MeasureSpace Ω'] (Y: Fin p.m × Fin p.m → Ω' → G) [IsFiniteMeasure hΩ'.volume] (hindep: iIndepFun _ Y) (hident: ∀ i, ∀ j, IdentDistrib (Y (i,j)) (X i) )
 
 local notation3 "W" => ∑ i, ∑ j, Y (i, j)
 local notation3 "Z1" => ∑ i: Fin p.m, ∑ j, (i:ℤ) • Y (i, j)
@@ -32,39 +34,28 @@ local notation3 "R" => fun r ↦ ∑ i, ∑ j, if (i+j+r = 0) then Y r else 0
 
 
 /--  Z_1+Z_2+Z_3= 0 -/
-lemma sum_of_z_eq_zero :
- let _ := p.hG; Z1 + Z2 + Z3 = 0 := sorry
+lemma sum_of_z_eq_zero :Z1 + Z2 + Z3 = 0 := sorry
 
-/--   We let
-  \[
-    \bbI[Z_1 : Z_2\, |\, W],\
-    \bbI[Z_2 : Z_3\, |\, W],\
-    \bbI[Z_1 : Z_3\, |\, W] \leq t
-  \]
-  where $t :=  4m^2 \eta k$.
+/--   We have `I[Z_1 : Z_2 | W], I[Z_2 : Z_3 | W], I[Z_1 : Z_3 | W] ≤  4m^2 η k`.
 -/
-lemma mutual_information_le_t_12 : let _ := p.hG; let _ := p.hGm; I[ Z1 : Z2 | W] ≤ 4 * (p.m)^2 * p.η * k := sorry
+lemma mutual_information_le_t_12 : I[ Z1 : Z2 | W] ≤ 4 * (p.m)^2 * p.η * k := sorry
 
-lemma mutual_information_le_t_13 : let _ := p.hG; let _ := p.hGm; I[ Z1 : Z3 | W] ≤ 4 * (p.m)^2 * p.η * k := sorry
+lemma mutual_information_le_t_13 : I[ Z1 : Z3 | W] ≤ 4 * (p.m)^2 * p.η * k := sorry
 
-lemma mutual_information_le_t_23 : let _ := p.hG; let _ := p.hGm; I[ Z2 : Z3 | W] ≤ 4 * (p.m)^2 * p.η * k := sorry
+lemma mutual_information_le_t_23 : I[ Z2 : Z3 | W] ≤ 4 * (p.m)^2 * p.η * k := sorry
 
 
 /-- We let $\bbH[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \bbH[X_i]$. -/
-lemma entropy_of_W_le : let _ := p.hG; let _ := p.hGm; H[W] ≤ (2*p.m - 1) * k + (m:ℝ)⁻¹ * ∑ i, H[X i] := sorry
+lemma entropy_of_W_le : H[W] ≤ (2*p.m - 1) * k + (m:ℝ)⁻¹ * ∑ i, H[X i] := sorry
 
 /-- We let $\bbH[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \bbH[X_i]$. -/
-lemma entropy_of_Z_two_le : let _ := p.hG; let _ := p.hGm; H[Z2] ≤ (8 * p.m^2 - 16 * p.m + 1) * k + (m:ℝ)⁻¹ * ∑ i, H[X i] := sorry
+lemma entropy_of_Z_two_le : H[Z2] ≤ (8 * p.m^2 - 16 * p.m + 1) * k + (m:ℝ)⁻¹ * ∑ i, H[X i] := sorry
 
 /-- We let  $\bbI[W : Z_2] \leq 2 (m-1) k$. -/
-lemma mutual_of_W_Z_two_le : let _ := p.hG; let _ := p.hGm; I[W : Z2] ≤ 2 * (p.m-1) * k := sorry
-
-example : let hGm := p.hGm; @MeasurableSingletonClass p.G hGm := by
-  let hGsc : @MeasurableSingletonClass p.G p.hGm := p.hGsc
-  exact hGsc
+lemma mutual_of_W_Z_two_le : I[W : Z2] ≤ 2 * (p.m-1) * k := sorry
 
 /-- We let $\sum_{i=1}^m d[X_i;Z_2|W] \leq 8(m^3-m^2) k$. -/
-lemma sum_of_conditional_distance_le : let _ := p.hG; let _ := p.hGm; let _ := p.hGsc; let _ := p.hGf; ∑ i, d[ X i # Z2 | W] ≤ 8 * (p.m^3 - p.m^2)*k := sorry
+lemma sum_of_conditional_distance_le : ∑ i, d[ X i # Z2 | W] ≤ 8 * (p.m^3 - p.m^2)*k := sorry
 
 
 /-- Let $G$ be an abelian group, let $(T_1,T_2,T_3)$ be a $G^3$-valued random variable such that $T_1+T_2+T_3=0$ holds identically, and write
@@ -81,6 +72,9 @@ lemma dist_of_U_add_le : 0 = 1 := sorry
 /-- We let $k = 0$. -/
 lemma k_eq_zero : k = 0 := sorry
 
+end AnalyzeMinimizer
+
+
 /-- Suppose that $G$ is a finite abelian group of torsion $m$.  Suppose that $X$ is a $G$-valued random variable. Then there exists a subgroup $H \leq G$ such that \[ d[X;U_H] \leq 64 m^3 d[X;X].\] -/
 lemma dist_of_X_U_H_le {G : Type*} [AddCommGroup G]  [Fintype G] [MeasurableSpace G]
   [MeasurableSingletonClass G] (m:ℕ) (hm: m ≥ 2) (htorsion: ∀ x:G, m • x = 0) (Ω: Type*) [MeasureSpace Ω] (X: Ω → G):  ∃ H : AddSubgroup G, ∃ Ω' : Type*, ∃ mΩ : MeasureSpace Ω', ∃ U : Ω' → G,