ent_bsg

lemma ent_bsg [IsProbabilityMeasure μ] {A B : Ω → G} (hA : Measurable A) (hB : Measurable B)    [Finite G] :    (μ.map (A + B))[fun z ↦ d[A ; μ[|(A + B) ⁻¹' {z}] # B ; μ[|(A + B) ⁻¹' {z}]]]      ≤ 3 * I[A : B; μ] + 2 * H[A + B ; μ] - H[A ; μ] - H[B ; μ] := by  let Z := A + B  have hZ : Measurable Z := hA.add hB  obtain ⟨Ω', _, AB₁, AB₂, Z', ν, _, hAB₁, hAB₂, hZ', hABZ, hABZ₁, hABZ₂, hZ₁, hZ₂⟩ :=    condIndep_copies' (⟨A, B⟩) Z (hA.prodMk hB) hZ μ (fun (a, b) c ↦ c = a + b)    .of_discrete (Eventually.of_forall fun _ ↦ rfl)  let A₁ := fun ω ↦ (AB₁ ω).1  let B₁ := fun ω ↦ (AB₁ ω).2  let A₂ := fun ω ↦ (AB₂ ω).1  let B₂ := fun ω ↦ (AB₂ ω).2  replace hZ₁ : Z' = A₁ + B₁ := funext hZ₁  replace hZ₂ : Z' = A₂ + B₂ := funext hZ₂  have hA₁ : Measurable A₁ := hAB₁.fst  have hB₁ : Measurable B₁ := hAB₁.snd  have hA₂ : Measurable A₂ := hAB₂.fst  have hB₂ : Measurable B₂ := hAB₂.snd  have hZZ' : IdentDistrib Z' Z ν μ := hABZ₁.comp measurable_snd  have :=    calc      H[⟨A₁, ⟨B₁, A₁ - B₂⟩⟩ ; ν]        = H[⟨⟨A₁, B₁⟩, ⟨⟨A₂, B₂⟩, Z'⟩⟩ ; ν] := entropy_of_comp_eq_of_comp _          (hA₁.prodMk <| hB₁.prodMk <| hA₁.sub hB₂) (hAB₁.prodMk <| hAB₂.prodMk hZ')            (fun (a, b, c) ↦ ((a, b), (b + c, a - c), a + b))            (fun ((a, b), (_c, d), _e) ↦ (a, b, a - d))          (by funext; simpa [sub_add_eq_add_sub, Prod.ext_iff, ← hZ₁, hZ₂, two_nsmul,            ← add_sub_assoc, add_comm, eq_sub_iff_add_eq]             using congr_fun (hZ₂.symm.trans hZ₁) _) rfl      _ = H[⟨⟨A₁, B₁⟩, Z'⟩ ; ν] + H[⟨⟨A₂, B₂⟩, Z'⟩ ; ν] - H[Z' ; ν] :=        ent_of_cond_indep _ hAB₁ hAB₂ hZ' hABZ      _ = 2 * H[⟨⟨A, B⟩, Z⟩ ; μ] - H[Z ; μ] := by        rw [two_mul]        congr 1        congr 1 <;> exact IdentDistrib.entropy_congr ‹_›        exact hZZ'.entropy_congr      _ = 2 * H[⟨A, B⟩ ; μ] - H[Z ; μ] := by        congr 2        exact entropy_prod_comp (hA.prodMk hB) _ fun x ↦ x.1 + x.2  have :=    calc      H[⟨A₁, A₁ - B₂⟩ ; ν]        = H[⟨A₁, B₂⟩ ; ν] := entropy_sub_right hA₁ hB₂ _      _ ≤ H[A₁ ; ν] + H[B₂ ; ν] := entropy_pair_le_add hA₁ hB₂ _      _ = H[A ; μ] + H[B ; μ] := by        congr 1        · exact (hABZ₁.comp measurable_fst.fst).entropy_congr        · exact (hABZ₂.comp measurable_fst.snd).entropy_congr  have :=    calc      H[⟨B₁, A₁ - B₂⟩ ; ν]        = H[⟨A₂, B₁⟩ ; ν] := by          rw [entropy_comm hB₁ (show Measurable (A₁ - B₂) from hA₁.sub hB₂),            ← entropy_sub_left' hA₂ hB₁, sub_eq_sub_iff_add_eq_add.2 <| hZ₁.symm.trans hZ₂]      _ ≤ H[A₂ ; ν] + H[B₁ ; ν] := entropy_pair_le_add hA₂ hB₁ _      _ = H[A ; μ] + H[B ; μ] := by        congr 1        · exact (hABZ₂.comp measurable_fst.fst).entropy_congr        · exact (hABZ₁.comp measurable_fst.snd).entropy_congr  have :=    calc     _ ≤ _ := entropy_triple_add_entropy_le ν hA₁ hB₁ (show Measurable (A₁ - B₂) from hA₁.sub hB₂)     _ ≤ _ := add_le_add ‹_› ‹_›  have :=    calc      H[A₁ - B₂ | Z' ; ν]        ≤ H[A₁ - B₂ ; ν] := condEntropy_le_entropy _ (hA₁.sub hB₂) hZ'      _ ≤ _ := le_sub_iff_add_le'.2 ‹_›      _ = 2 * I[A : B ; μ] + H[Z ; μ] := by        rw [‹H[⟨A₁, ⟨B₁, A₁ - B₂⟩⟩ ; ν] = _›, mutualInfo_def]; ring  have hA₁Z :=    calc      H[A₁ | Z' ; ν]      _ = H[⟨A₁, B₁⟩ ; ν] - H[Z' ; ν] := by        rw [chain_rule'', hZ₁, entropy_add_right, entropy_comm] <;> assumption      _ = H[⟨A, B⟩ ; μ] - H[Z ; μ] := by        congr 1        · exact (hABZ₁.comp measurable_fst).entropy_congr        · exact hZZ'.entropy_congr      _ = H[A ; μ] + H[B ; μ] - I[A : B ; μ] - H[Z ; μ] := by        rw [← entropy_add_entropy_sub_mutualInfo]  have hB₂Z :=    calc      H[B₂ | Z' ; ν]      _ = H[⟨A₂, B₂⟩ ; ν] - H[Z' ; ν] := by        rw [chain_rule'', hZ₂, entropy_add_right', entropy_comm] <;> assumption      _ = H[⟨A, B⟩ ; μ] - H[Z ; μ] := by        congr 1        · exact (hABZ₂.comp measurable_fst).entropy_congr        · exact hZZ'.entropy_congr      _ = H[A ; μ] + H[B ; μ] - I[A : B ; μ] - H[Z ; μ] := by        rw [← entropy_add_entropy_sub_mutualInfo]  calc    (μ.map Z)[fun z ↦ d[A ; μ[|Z ← z] # B ; μ[|Z ← z]]]      = (ν.map Z')[fun z ↦ d[A₁ ; ν[|Z' ← z] # B₂ ; ν[|Z' ← z]]] := by        rw [hZZ'.map_eq]        refine integral_congr_ae <| Eventually.of_forall fun z ↦ ?_        have hAA₁ : IdentDistrib A₁ A (ν[|Z' ← z]) (μ[|Z ← z]) :=          (hABZ₁.comp <| measurable_fst.fst.prodMk measurable_snd).cond            (.singleton z) hZ' hZ        have hBB₂ : IdentDistrib B₂ B (ν[|Z' ← z]) (μ[|Z ← z]) :=          (hABZ₂.comp <| measurable_fst.snd.prodMk measurable_snd).cond            .of_discrete hZ' hZ        dsimp (config := {zeta := false}) [rdist]        rw [← hAA₁.entropy_congr, ← hBB₂.entropy_congr, hAA₁.map_eq, hBB₂.map_eq]    _ = (ν.map Z')[fun z ↦          H[A₁ - B₂ ; ν[|Z' ← z]] - H[A₁ ; ν[|Z' ← z]]/2 - H[B₂ ; ν[|Z' ← z]]/2] := by        apply integral_congr_ae        apply hABZ.mono        intro z hz        exact (hz.comp measurable_fst measurable_snd).rdist_eq hA₁ hB₂    _ = H[A₁ - B₂ | Z' ; ν] - H[A₁ | Z' ; ν] / 2 - H[B₂ | Z' ; ν] / 2 := by        rw [integral_sub, integral_sub, integral_div, integral_div]        · rfl        all_goals exact .of_finite    _ ≤ 2 * I[A : B ; μ] + H[Z ; μ] - H[A₁ | Z' ; ν] / 2 - H[B₂ | Z' ; ν] / 2 :=        sub_le_sub_right (sub_le_sub_right ‹_› _) _    _ = _ := by rw [hA₁Z, hB₂Z]; ring