Source indexedlemma · leanprover/lean4:v4.33.0-rc1

construct_good_prelim

PFR.Endgame · PFR/Endgame.lean:352 to 401

Source documentation

If $T_1, T_2, T_3$ are $G$ -valued random variables with $T_1+T_2+T_3=0$ holds identically and $\delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$ Then there exist random variables $T'_1, T'_2$ such that $d[T'_1;T'_2] + \eta (d[X_1^0;T'_1] - d[X_1^0;X_1]) + \eta(d[X_2^0;T'_2] - d[X_2^0;X_2])$ is at most $\delta + \eta ( d[X^0_1;T_1]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2]-d[X^0_2;X_2])$ $+ \tfrac12 \eta I[T_1: T_3] + \tfrac12 \eta I[T_2: T_3].$

Exact Lean statement

lemma construct_good_prelim :
    k ≤ δ + p.η * c[T₁ # T₂] + p.η * (I[T₁: T₃] + I[T₂ : T₃])/2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma construct_good_prelim :    k ≤ δ + p.η * c[T₁ # T₂] + p.η * (I[T₁: T₃] + I[T₂ : T₃])/2 := by  let sum1 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[T₁; ℙ[|T₃ ⁻¹' {t}] # T₂; ℙ[|T₃ ⁻¹' {t}]]]  let sum2 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[p.X₀₁; ℙ # T₁; ℙ[|T₃ ⁻¹' {t}]] - d[p.X₀₁ # X₁]]  let sum3 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ d[p.X₀₂; ℙ # T₂; ℙ[|T₃ ⁻¹' {t}]] - d[p.X₀₂ # X₂]]  let sum4 : ℝ := (Measure.map T₃ ℙ)[fun t ↦ ψ[T₁; ℙ[|T₃ ⁻¹' {t}] # T₂; ℙ[|T₃ ⁻¹' {t}]]]  have hp.η : 0 ≤ p.η := by linarith [p.hη]  have hP : IsProbabilityMeasure (Measure.map T₃ ℙ) :=    Measure.isProbabilityMeasure_map hT₃.aemeasurable  have h2T₃ : T₃ = T₁ + T₂ :=    calc T₃ = T₁ + T₂ + T₃ - T₃ := by rw [hT, zero_sub]; simp [ZModModule.neg_eq_self]      _ = T₁ + T₂ := by rw [add_sub_cancel_right]  have h2T₁ : T₁ = T₂ + T₃ := by simp [h2T₃, add_left_comm, ZModModule.add_self]  have h2T₂ : T₂ = T₃ + T₁ := by simp [h2T₁, add_left_comm, ZModModule.add_self]  have h1 : sum1 ≤ δ := by    have h1 : sum1 ≤ 3 * I[T₁ : T₂] + 2 * H[T₃] - H[T₁] - H[T₂] := by      subst h2T₃; exact ent_bsg hT₁ hT₂    have h2 : H[⟨T₂, T₃⟩] = H[⟨T₁, T₂⟩] := by      rw [h2T₃, entropy_add_right', entropy_comm] <;> assumption    have h3 : H[⟨T₁, T₂⟩] = H[⟨T₃, T₁⟩] := by      rw [h2T₃, entropy_add_left, entropy_comm] <;> assumption    simp_rw [mutualInfo_def] at h1 ⊢; linarith  have h2 : p.η * sum2 ≤ p.η * (d[p.X₀₁ # T₁] - d[p.X₀₁ # X₁] + I[T₁ : T₃] / 2) := by    have : sum2 = d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁] := by      simp only [integral_sub .of_finite .of_finite, integral_const, smul_eq_mul, sum2]      simp [condRuzsaDist'_eq_sum hT₁ hT₃, integral_eq_setIntegral        (FiniteRange.ae_mem_toFinset _ T₃), setIntegral_finset _ .finset,        map_measureReal_apply hT₃ (.singleton _)]    gcongr    linarith [condRuzsaDist_le' ℙ ℙ p.hmeas1 hT₁ hT₃]  have h3 : p.η * sum3 ≤ p.η * (d[p.X₀₂ # T₂] - d[p.X₀₂ # X₂] + I[T₂ : T₃] / 2) := by    have : sum3 = d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂] := by      simp only [integral_sub .of_finite .of_finite, integral_const, smul_eq_mul, sum3]      simp [condRuzsaDist'_eq_sum hT₂ hT₃,        integral_eq_setIntegral (FiniteRange.ae_mem_toFinset _ T₃),         setIntegral_finset _ .finset,        map_measureReal_apply hT₃ (.singleton _)]    gcongr    linarith [condRuzsaDist_le' ℙ ℙ p.hmeas2 hT₂ hT₃]  have h4 : sum4 ≤ δ + p.η * c[T₁ # T₂] + p.η * (I[T₁ : T₃] + I[T₂ : T₃]) / 2 := by    suffices sum4 = sum1 + p.η * (sum2 + sum3) by linarith    simp only [sum1, sum2, sum3, sum4, integral_add .of_finite .of_finite, integral_const_mul]  have hk : k ≤ sum4 := by    suffices (Measure.map T₃ ℙ)[fun _ ↦ k] ≤ sum4 by simpa using this    refine integral_mono_ae .of_finite .of_finite <| ae_iff_of_countable.2 fun t ht ↦ ?_    have : IsProbabilityMeasure (ℙ[|T₃ ⁻¹' {t}]) :=      cond_isProbabilityMeasure (by simpa [hT₃] using ht)    dsimp only    linarith only [distance_ge_of_min' (μ := ℙ[|T₃ ⁻¹' {t}]) (μ' := ℙ[|T₃ ⁻¹' {t}]) p h_min hT₁ hT₂]  exact hk.trans h4