nonnegativity of cond multidistance

teorth · Nov 4, 2024 · 514591d · 514591d
1 parent 26d310b
commit 514591d
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 10 deletions.
diff --git a/PFR/MoreRuzsaDist.lean b/PFR/MoreRuzsaDist.lean
@@ -933,15 +933,20 @@ theorem condMultiDist_nonneg [Fintype G] {m : ℕ} {Ω : Fin m → Type*} (hΩ :
   dsimp [condMultiDist]
   apply Finset.sum_nonneg
   intro y _
-  apply mul_nonneg
-  . apply Finset.prod_nonneg
-    intro i _
-    exact ENNReal.toReal_nonneg
-  have (i : Fin m) : ℙ (Y i ⁻¹' {y i}) ≠ 0 := by
-    -- This probably requires additional assumptions on Y.
-    sorry
-  exact multiDist_nonneg (fun i => ⟨ℙ[|Y i ⁻¹' {y i}]⟩)
-    (fun i => ProbabilityTheory.cond_isProbabilityMeasure (this i)) X hX
+  by_cases h: ∀ i : Fin m, ℙ (Y i ⁻¹' {y i}) ≠ 0
+  . apply mul_nonneg
+    . apply Finset.prod_nonneg
+      intro i _
+      exact ENNReal.toReal_nonneg
+    exact multiDist_nonneg (fun i => ⟨ℙ[|Y i ⁻¹' {y i}]⟩)
+      (fun i => ProbabilityTheory.cond_isProbabilityMeasure (h i)) X hX
+  simp only [ne_eq, not_forall, Decidable.not_not] at h
+  obtain ⟨i, hi⟩ := h
+  apply le_of_eq
+  symm
+  convert zero_mul ?_
+  apply Finset.prod_eq_zero (Finset.mem_univ i)
+  simp only [hi, ENNReal.zero_toReal]
 
 /-- A technical lemma: can push a constant into a product at a specific term -/
 private lemma Finset.prod_mul {α β:Type*} [Fintype α] [DecidableEq α] [CommMonoid β] (f:α → β) (c: β) (i₀:α) : (∏ i, f i) * c = ∏ i, (if i=i₀ then f i * c else f i) := calc

diff --git a/blueprint/src/chapter/torsion.tex b/blueprint/src/chapter/torsion.tex
@@ -333,7 +333,7 @@ \section{The tau functional}
 \begin{lemma}[Conditional multidistance nonnegative]\label{cond-multidist-nonneg}\uses{cond-multidist-def}\lean{condMultiDist_nonneg}\leanok If $X_{[m]} = (X_i)_{1 \leq i \leq m}$ and $Y_{[m]} = (Y_i)_{1 \leq i \leq m}$ are tuples of random variables, then $D[ X_{[m]} | Y_{[m]} ] \geq 0$.
 \end{lemma}
 
-\begin{proof}\uses{multidist-nonneg} Clear from \Cref{multidist-nonneg} and \Cref{cond-multidist-def}, except that some care may need to be taken to deal with the $y_i$ where $p_{Y_i}$ vanish.
+\begin{proof}\uses{multidist-nonneg}\leanok Clear from \Cref{multidist-nonneg} and \Cref{cond-multidist-def}, except that some care may need to be taken to deal with the $y_i$ where $p_{Y_i}$ vanish.
 \end{proof}