Dist of U add le

lemma dist_of_U_add_le {G : Type*} [MeasurableFinGroup G] {Ω : Type u} [hΩ : MeasureSpace Ω]    [IsProbabilityMeasure (ℙ : Measure Ω)] {T₁ T₂ T₃ : Ω → G} (hsum : T₁ + T₂ + T₃ = 0)    (hmes₁ : Measurable T₁) (hmes₂ : Measurable T₂) (hmes₃ : Measurable T₃) {n : ℕ}    {Ω' : Fin n → Type*} (hΩ' : ∀ i, MeasureSpace (Ω' i)) [∀ i, IsProbabilityMeasure (hΩ' i).volume]    {Y : ∀ i, (Ω' i) → G} (hY : ∀ i, Measurable (Y i)) {α : ℝ} (hα : α > 0) :    ∃ (Ω'' : Type u) (hΩ'': MeasureSpace Ω'') (U: Ω'' → G),      IsProbabilityMeasure hΩ''.volume ∧ Measurable U ∧        d[U # U] + α * ∑ i, d[Y i # U] ≤          (2 + α * n / 2) * (I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]) + α * ∑ i, d[Y i # T₂] := by  let δ := I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]  have h1 := ent_bsg (μ := ℙ) hmes₁ hmes₂  have h₁₂ : I[T₁ : T₂] = H[T₁] + H[T₂] - H[ ⟨T₁, T₂⟩ ] := mutualInfo_def _ _ _  have h₁₃ : I[T₁ : T₃] = H[T₁] + H[T₃] - H[ ⟨T₁, T₃⟩ ] := mutualInfo_def _ _ _  have h₂₃ : I[T₂ : T₃] = H[T₂] + H[T₃] - H[ ⟨T₂, T₃⟩ ] := mutualInfo_def _ _ _  have h₃_neg : H[T₁+T₂] = H[T₃] := by    rw [← entropy_neg (by fun_prop)]; congr; rwa [← add_eq_zero_iff_neg_eq]  have h₁₃_eq : H[ ⟨T₁, T₃⟩ ] = H[ ⟨T₁, T₂⟩ ] := by    rw [←entropy_add_right', ←entropy_neg_right] <;> try fun_prop    congr!; rw [←add_eq_zero_iff_neg_eq, ←hsum]; abel  have h₂₃_eq : H[ ⟨T₁, T₃⟩ ] = H[ ⟨T₂, T₃⟩ ] := by    rw [←entropy_add_left', ←entropy_neg_left] <;> try fun_prop    congr!; rw [←add_eq_zero_iff_neg_eq, ←hsum]; abel  let _hG : MeasureSpace G := ⟨Measure.map (T₁ + T₂) ℙ⟩  let _ : IsProbabilityMeasure (ℙ: Measure G) := Measure.isProbabilityMeasure_map (by fun_prop)  change    ∫ x, (fun z ↦ d[T₁ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂; ℙ[|(T₁ + T₂) ⁻¹' {z}]]) x ≤      3 * I[T₁ : T₂] + 2 * H[T₁ + T₂] - H[T₁] - H[T₂] at h1  replace h1 : ∫ z, 2 * d[T₁ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] ≤ 2 * δ := by    rw [integral_const_mul_of_integrable .of_finite]; linarith  replace h1 : ∫ (z : G), d[T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] ≤ 2 * δ := by    apply LE.le.trans _ h1    apply integral_mono <;> try apply MeasureTheory.Integrable.of_finite    intro z    by_cases h : ℙ ( (T₁+T₂) ⁻¹' {z} ) = 0    · simp [cond_eq_zero_of_meas_eq_zero h, rdist_def]    have : IsProbabilityMeasure ℙ[|(T₁ + T₂) ⁻¹' {z}] := cond_isProbabilityMeasure h    calc      _ ≤ d[T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₁ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] +           d[T₁ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] :=        rdist_triangle (by fun_prop) (by fun_prop) (by fun_prop)      _ ≤ d[T₁ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] +            d[T₁ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂ ; ℙ[|(T₁+ T₂) ⁻¹' {z}]] := by rw [rdist_symm]      _ = _ := by ring  have h2 (i:Fin n): ∫ (z : G), d[Y i ; ℙ # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] ≤ d[Y i # T₂] + δ/2 := calc    _ = d[Y i # T₂ | T₃] := by      rw [condRuzsaDist'_eq_sum', integral_fintype .of_finite] <;> try fun_prop      classical      trans ∑ x ∈ -Finset.univ, (ℙ:Measure G).real {x} • d[Y i ; ℙ # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {x}]]      · simp      rw [Finset.sum_neg_index]      apply Finset.sum_congr rfl; intro x      have : (T₁ + T₂) ⁻¹' {-x} = T₃ ⁻¹' {x} := by        rw [add_eq_zero_iff_eq_neg] at hsum; rw [hsum]        ext ω; simp      unfold _hG      simp only [Finset.mem_univ, smul_eq_mul, forall_const]      rw [map_measureReal_apply, this]      · fun_prop      measurability    _ ≤ d[Y i # T₂] + I[T₂ : T₃]/2 := by      convert condRuzsaDist_le' _ _ _ _ _ <;> try infer_instance      all_goals fun_prop    _ ≤ d[Y i # T₂] + δ / 2 := by      gcongr      have : I[T₁ : T₂] ≥ 0 := by apply mutualInfo_nonneg <;> try fun_prop      have : I[T₁ : T₃] ≥ 0 := by apply mutualInfo_nonneg <;> try fun_prop      linarith  set F : G → ℝ := fun z ↦ d[T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] +      α * ∑ i, d[Y i ; ℙ # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]]  have h3 : ∫ (z : G), F z ≤ 2 * δ + α * ∑ i, d[Y i # T₂] + α * n * δ / 2:= calc    _ = ∫ (z : G), d[T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}] # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] ∂ℙ +        α * ∑ i, ∫ (z : G), d[Y i ; ℙ # T₂ ; ℙ[|(T₁ + T₂) ⁻¹' {z}]] := by      rw [integral_add, integral_const_mul,integral_finsetSum] <;> try intros      all_goals apply MeasureTheory.Integrable.of_finite    _ ≤ _ := by      rw [add_assoc]; gcongr; calc        _ ≤ α * ∑ i, (d[Y i # T₂] + δ/2) := by          gcongr with i; exact h2 i        _ = _ := by          simp [Finset.sum_add_distrib]; ring  obtain ⟨z, hz, hpos⟩ := pigeonhole F  replace h3 := hz.trans h3  use Ω, ⟨ℙ[|(T₁ + T₂) ⁻¹' {z}]⟩, T₂  refine ⟨?_, ?_, ?_⟩  · apply cond_isProbabilityMeasure    convert hpos    unfold _hG    dsimp    rw [Measure.map_apply (by fun_prop) (by measurability)]  · fun_prop  convert! h3 using 1  ring