k_eq_zero

lemma k_eq_zero (hη_eq : p.η = 1 / (32 * p.m ^ 3)) : k = 0 := by  let hm := p.hm  let hη := p.hη  let zero : Fin p.m := ⟨0, by linarith only [hm]⟩  let δ (w : G) : ℝ :=    I[Z1 : Z2 ; ℙ[|W ⁻¹' {w}]] + I[Z1 : Z3 ; ℙ[|W ⁻¹' {w}]] + I[Z2 : Z3 ; ℙ[|W ⁻¹' {w}]]  have hδ_int : ∫ w, δ w ∂(Measure.map W ℙ) ≤ 3*p.m*(4*p.m+1)*p.η*k := by    unfold δ    rw [integral_add, integral_add] <;> try apply Integrable.of_finite    simp_rw [←condMutualInfo_eq_integral_mutualInfo]    calc      _ ≤ p.m * (4*p.m+1) * p.η * k + p.m * (4*p.m+1) * p.η * k + p.m * (4*p.m+1) * p.η * k := by        gcongr        · exact mutual_information_le_t_12 hΩ h_min h_mes h_indep hident        · exact mutual_information_le_t_13 hΩ h_min h_mes h_indep hident        exact mutual_information_le_t_23 hΩ h_min h_mes h_indep hident      _ = _ := by ring  let _ : MeasureSpace G := ⟨Measure.map W ℙ⟩  have _ : IsProbabilityMeasure (ℙ: Measure G) := Measure.isProbabilityMeasure_map (by fun_prop)  let δ' : G → ℝ := fun w ↦ p.m * (2 + p.η / 2) * (δ w) + p.η * ∑ i, d[X i ; ℙ # Z2 ; ℙ[|W ⁻¹' {w}]]  have main_est {w:G} (hw: ℙ {w} ≠ 0) : k ≤ δ' w := by    let μ : Measure Ω' := ℙ[|W ⁻¹' {w}]    have hμ_prob : IsProbabilityMeasure μ := by      apply cond_isProbabilityMeasure; convert hw      symm; apply MeasureTheory.Measure.map_apply (by fun_prop) (MeasurableSet.singleton _)    obtain ⟨Ω'', hΩ'', U, hΩ''_prob, hU_mes, h_ineq⟩ :=      @dist_of_U_add_le G inferInstance Ω' ⟨μ⟩ hμ_prob Z1 Z2 Z3 sum_of_z_eq_zero      (by fun_prop) (by fun_prop) (by fun_prop) p.m Ω hΩ hΩ_prob X hX_mes (p.η/p.m) (by positivity)    have h1 : D[fun i:Fin p.m ↦ U; fun _ ↦ hΩ''] ≤ p.m * d[U # U] := by      apply multidist_ruzsa_III hm (i₀ := zero) <;> try infer_instance      · intros; apply IdentDistrib.refl; fun_prop      fun_prop    have h2 : k - D[fun i:Fin p.m ↦ U; fun _ ↦ hΩ''] ≤ p.η * ∑ i, d[X i # U] := by      convert sub_multiDistance_le _ _ h_min _ _ <;> try infer_instance      all_goals fun_prop    have h3 : p.m * d[U # U] + p.η * ∑ i, d[X i # U] ≤      p.m * (2 + p.η / 2) * (δ w) + p.η * ∑ i, d[X i ; ℙ # Z2 ; ℙ[|W ⁻¹' {w}]] := calc        _ = p.m * (d[U # U] + p.η / p.m * ∑ i, d[X i # U]) := by field_simp        _ ≤ p.m * ((2 + p.η / ↑p.m * ↑p.m / 2) * (I[Z1 : Z2; μ] + I[Z1 : Z3; μ] + I[Z2 : Z3; μ]) +              p.η / ↑p.m * ∑ i, d[X i; ℙ # Z2; μ]) := by gcongr _ * ?_; exact h_ineq        _ = p.m * ((2 + p.η / p.m * p.m / 2) *              δ w + p.η / p.m * ∑ i, d[X i ; ℙ # Z2 ; ℙ[|W ⁻¹' {w}]]) := rfl        _ = _ := by field_simp    unfold δ'    linarith only [h1, h2, h3]  replace main_est : k ≤ ∫ w, δ' w := by    obtain ⟨w, hwδ, hw⟩ := pigeonhole δ'    specialize main_est hw; order  have integ_eq :      ∫ w, δ' w ≤        p.m * (2 + p.η / 2) * (3*p.m*(4*p.m+1)*p.η*k) + p.η * (4 * (p.m^3 - p.m^2)*k) := by    unfold δ'    rw [integral_add, integral_const_mul, integral_const_mul, MeasureTheory.integral_finsetSum] <;>      try intros; apply Integrable.of_finite    gcongr    · exact hδ_int    convert! sum_of_conditional_distance_le hΩ hΩ_prob hX_mes h_mes h_indep hident with i _    symm    exact condRuzsaDist'_eq_integral _ (by fun_prop) (by fun_prop) _ _  by_contra!  replace this : k > 0 := by have : k ≥ 0 := multiDist_nonneg _ hΩ_prob _ hX_mes; order  have h4 :      1 ≤ p.m * (2 + p.η / 2) * (3 * p.m * (4 * p.m + 1) * p.η) + p.η * (4 * (p.m^3 - p.m^2)) := by    rw [← mul_le_mul_iff_of_pos_right  this]    calc      _ ≤ p.m * (2 + p.η / 2) * (3 * p.m * (4 * p.m + 1) * p.η * k)          + p.η * (4 * (p.m^3 - p.m^2)*k) := by linarith only [main_est, integ_eq]      _ = _ := by ring  have h5 :      p.m * (2 + p.η / 2) * (3 * p.m * (4 * p.m + 1) * p.η) + p.η * (4 * (p.m^3 - p.m^2)) < 1 := by    calc      _ ≤ p.m * (2 + (1/32) / 2) * (3 * p.m * (4 * p.m + p.m/2) * p.η) + p.η * (4 * p.m^3) := by        rw [hη_eq]; gcongr        · norm_cast; simp; linarith only [Nat.pow_le_pow_left hm 3]        · norm_cast; linarith only [show p.m ≥ (2:ℝ) by simpa]        simp      _ < _ := by        rw [hη_eq]        field_simp        ring_nf        norm_num  order