weak_PFR_asymm_prelim

lemma weak_PFR_asymm_prelim (A B : Set G) [A_fin : Finite A] [B_fin : Finite B]    (hnA : A.Nonempty) (hnB : B.Nonempty) :    ∃ (N : AddSubgroup G) (x y : G ⧸ N) (Ax By : Set G), Ax.Nonempty ∧ By.Nonempty ∧    Set.Finite Ax ∧ Set.Finite By ∧ Ax = {z : G | z ∈ A ∧ QuotientAddGroup.mk' N z = x } ∧    By = {z : G | z ∈ B ∧ QuotientAddGroup.mk' N z = y } ∧    (log 2) * Module.finrank ℤ G ≤ log (Nat.card (G ⧸ N)) +      40 * dᵤ[A # B ] ∧ log (Nat.card A) + log (Nat.card B) - log (Nat.card Ax) - log (Nat.card By)      ≤ 34 * (dᵤ[A # B ] - dᵤ[Ax # By ]) := by  have : Nonempty A := hnA.to_subtype  have : Nonempty B := hnB.to_subtype  set ψ : G →+ G := zsmulAddGroupHom 2  set G₂ := LinearMap.range (LinearMap.lsmul ℤ G 2)  set H := ModN G 2  set φ : G →ₗ[ℤ] H := G₂.mkQ  let _mH : MeasurableSpace H := ⊤  have : Finite H := ModN.instFinite  let h_fintype : Fintype H := .ofFinite H  have : IsAddTorsionFree G :=.of_isTorsionFree ℤ _  obtain ⟨Ω, mΩ, UA, hμ, hUA_mes, hUA_unif, hUA_mem, hUA_fin⟩ :=    exists_isUniform_measureSpace' A A_fin hnA  obtain ⟨Ω', mΩ', UB, hμ', hUB_mes, hUB_unif, hUB_mem, hUB_fin⟩ :=    exists_isUniform_measureSpace' B B_fin hnB  obtain ⟨H', hH1, hH2⟩ := PFR_projection (φ ∘ UA) (φ ∘ UB) ℙ ℙ (by fun_prop) (by fun_prop)  let N := AddSubgroup.comap φ.toAddMonoidHom H'.toAddSubgroup  set φ' := QuotientAddGroup.mk' N  have _cGN : Countable (G ⧸ N) := Surjective.countable (QuotientAddGroup.mk'_surjective N)  have _msGN : MeasurableSingletonClass (G ⧸ N) :=    ⟨fun x ↦ MeasurableSpace.map_def.mpr .of_discrete⟩  rcases third_iso H'.toAddSubgroup with ⟨e : H ⧸ H' ≃+ G ⧸ N, he⟩  rcases single_fibres φ' hnA hnB hUA_mes hUB_mes hUA_unif hUB_unif hUA_mem hUB_mem with    ⟨x, y, Ax, By, hAx, hBy, hnAx, hnBy, hcard_ineq⟩  have : Nonempty Ax := hnAx.to_subtype  have : Nonempty By := hnBy.to_subtype  have Axf : Finite Ax := by rw [hAx]; infer_instance  have Byf : Finite By := by rw [hBy]; infer_instance  have h1 := torsion_dist_shrinking (G := G) (H := H) UA UB ℙ ℙ hUA_mes hUB_mes φ  have h2 := torsion_dist_shrinking (G := G) (H := H) UB UA ℙ ℙ hUB_mes hUA_mes φ  rw [rdist_symm] at h2  rw [← setRuzsaDist_eq_rdist hUA_unif hUB_unif hUA_mes hUB_mes] at h1 h2  -- using explicit .toFun casts as this saves a lot of heartbeats  change H[φ ∘ UA] ≤ 10 * dᵤ[A # B] at h1  change H[φ ∘ UB] ≤ 10 * dᵤ[A # B] at h2  replace hH1 : log (Nat.card H') ≤ 40 * dᵤ[A # B] := by    apply hH1.trans    linarith  replace h_card : log 2 * Module.finrank ℤ G      ≤ log (Nat.card (G ⧸ N)) + 40 * dᵤ[A # B] := by    rw [mul_comm, ← log_rpow (by norm_num)]    norm_cast    classical    rwa [← ModN.natCard_eq, ← Nat.card_congr e.toEquiv, H'.card_eq_card_quotient_mul_card,      Nat.cast_mul, log_mul, add_comm, add_le_add_iff_left]    all_goals norm_cast; rw [Nat.card_eq_fintype_card]; exact Fintype.card_ne_zero  use N, x, y, Ax, By  refine ⟨hnAx, hnBy, Ax.toFinite, By.toFinite, hAx, hBy, h_card, ?_⟩  replace hH2 : H[φ'.toFun ∘ UA] + H[φ'.toFun ∘ UB] ≤ 34 * d[φ'.toFun ∘ UA # φ'.toFun ∘ UB] := by    set X := (H'.mkQ.toFun ∘ φ.toFun) ∘ UA    set Y := (H'.mkQ.toFun ∘ φ.toFun) ∘ UB    have hX : Measurable X := Measurable.comp .of_discrete hUA_mes    have hY : Measurable Y := Measurable.comp .of_discrete hUB_mes    change H[X] + H[Y] ≤ 34 * d[X # Y] at hH2    have ha : φ'.toFun ∘ UA = e.toFun ∘ X := by ext x; exact (he (UA x)).symm    have hb : φ'.toFun ∘ UB = e.toFun ∘ Y := by ext x; exact (he (UB x)).symm    have he_inj : Injective e.toFun := e.injective    rw [ha, hb, entropy_comp_of_injective _ hX _ he_inj, entropy_comp_of_injective _ hY _ he_inj]    have : d[e.toFun ∘ X # e.toFun ∘ Y] = d[X # Y] := rdist_of_inj hX hY e.toAddMonoidHom he_inj    rwa [this]  set X : Ω → G ⧸ N := φ'.toFun ∘ UA  set Y : Ω' → G ⧸ N := φ'.toFun ∘ UB  have hX : Measurable X := Measurable.comp .of_discrete hUA_mes  have hY : Measurable Y := Measurable.comp .of_discrete hUB_mes  rcases le_iff_lt_or_eq.mp (rdist_nonneg (μ := ℙ) (μ' := ℙ) hX hY) with h | h  swap  · rw [← h] at hH2    have hH2A : H[X] ≥ 0 := entropy_nonneg _ _    have hH2B : H[Y] ≥ 0 := entropy_nonneg _ _    have hH2A' : H[X] ≤ 0 := by linarith only [hH2, hH2A, hH2B]    have hH2B' : H[Y] ≤ 0 := by linarith only [hH2, hH2A, hH2B]    rcases const_of_nonpos_entropy (μ := ℙ) hX hH2A' with ⟨x', hx⟩    rcases const_of_nonpos_entropy (μ := ℙ) hY hH2B' with ⟨y', hy⟩    have hAAx {z : G} (hz : z ∈ A) : φ'.toFun z = x' := by      change (ℙ).real (UA⁻¹' (φ'⁻¹' {x'})) = 1 at hx      rw [← MeasureTheory.map_measureReal_apply hUA_mes .of_discrete] at hx      set Af := A.toFinite.toFinset      have hUAf : IsUniform Af UA := by        convert hUA_unif; simp only [Af, Set.Finite.coe_toFinset]      have hnAf : 0 < Nat.card Af := by simp only [Af, Set.Finite.mem_toFinset, Nat.card_pos]      have hzf : z ∈ Af := by simp [Af, Set.Finite.mem_toFinset, hz]      have : (Measure.map UA ℙ).real {z} > 0 := by        rw [IsUniform.measureReal_preimage_of_mem' hUAf hUA_mes hzf]        simp only [one_div, gt_iff_lt, inv_pos, Nat.cast_pos, Finset.card_pos]        exact (Finite.toFinset_nonempty (toFinite A)).mpr hnA      have _ : IsProbabilityMeasure ((ℙ).map UA) :=        Measure.isProbabilityMeasure_map (Measurable.aemeasurable hUA_mes)      replace this := single ((ℙ).map UA) hx this      rwa [Set.mem_preimage, Set.mem_singleton_iff] at this    have hxx : Ax = A := by      have h : hnAx.some ∈ Ax := hnAx.some_mem      simp only [hAx, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, mem_inter_iff, mem_preimage,        mem_singleton_iff, inter_eq_left] at h ⊢      have := hAAx h.1      simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, h.2] at this      intro z hz      simp only [this, mem_preimage, mem_singleton_iff]      exact hAAx hz    have hBBy {z : G} (hz : z ∈ B) : φ'.toFun z = y' := by      change (ℙ).real (UB⁻¹' (φ'⁻¹' {y'})) = 1 at hy      rw [← MeasureTheory.map_measureReal_apply hUB_mes .of_discrete] at hy      set Bf := B.toFinite.toFinset      have hUBf : IsUniform Bf UB := by convert hUB_unif; simp only [Bf, Set.Finite.coe_toFinset]      have hnBf : 0 < Nat.card Bf := by simp only [Bf, Set.Finite.mem_toFinset, Nat.card_pos]      have hzf : z ∈ Bf := by simp [Bf, Set.Finite.mem_toFinset, hz]      have : (Measure.map UB ℙ).real {z} > 0 := by        rw [IsUniform.measureReal_preimage_of_mem' hUBf hUB_mes hzf]        simp only [one_div, gt_iff_lt, inv_pos, Nat.cast_pos, Finset.card_pos]        exact (Finite.toFinset_nonempty (toFinite B)).mpr hnB      have _ : IsProbabilityMeasure ((ℙ).map UB) :=        Measure.isProbabilityMeasure_map (Measurable.aemeasurable hUB_mes)      replace this := single ((ℙ).map UB) hy this      rwa [Set.mem_preimage, Set.mem_singleton_iff] at this    have hyy : By = B := by      have h : hnBy.some ∈ By := hnBy.some_mem      simp only [hBy, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, mem_inter_iff, mem_preimage,        mem_singleton_iff, inter_eq_left] at h ⊢      have := hBBy h.1      simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, h.2] at this      intro z hz      simp only [this, mem_preimage, mem_singleton_iff]      exact hBBy hz    simp [hxx, hyy]  have := calc d[φ'.toFun ∘ UA # φ'.toFun ∘ UB] *    (log (Nat.card A) + log (Nat.card B) - log (Nat.card Ax) - log (Nat.card By))    _ = d[φ'.toFun ∘ UA # φ'.toFun ∘ UB] *        log (Nat.card A * Nat.card B / ((Nat.card Ax) * (Nat.card By))) := by      congr      convert (four_logs ?_ ?_ ?_ ?_).symm      all_goals norm_cast; exact Nat.card_pos    _ ≤ (H[φ'.toFun ∘ UA] + H[φ'.toFun ∘ UB]) * (d[UA # UB] - dᵤ[Ax # By]) := hcard_ineq    _ ≤ (34 * d[φ'.toFun ∘ UA # φ'.toFun ∘ UB]) * (d[UA # UB] - dᵤ[Ax # By]) := by      apply mul_le_mul_of_nonneg_right hH2      have := rdist_le_avg_ent (Measurable.comp (.of_discrete (f := φ'.toFun)) hUA_mes)        (Measurable.comp (.of_discrete (f := φ'.toFun)) hUB_mes)      replace this : 0 < H[φ'.toFun ∘ UA] + H[φ'.toFun ∘ UB] := by linarith      rw [← mul_le_mul_iff_right₀ this]      apply le_trans _ hcard_ineq      rw [mul_zero]      change 0 ≤ d[φ'.toFun ∘ UA # φ'.toFun ∘ UB]        * log (Nat.card A * Nat.card B / ((Nat.card Ax) * (Nat.card By)))      rw [← mul_zero d[φ'.toFun ∘ UA # φ'.toFun ∘ UB], mul_le_mul_iff_right₀ h]      apply Real.log_nonneg      rw [one_le_div (mod_cast mul_pos Nat.card_pos Nat.card_pos)]      gcongr      · apply Nat.card_mono (Set.toFinite A) (hAx ▸ Set.inter_subset_left)      · apply Nat.card_mono (Set.toFinite B) (hBy ▸ Set.inter_subset_left)    _ = d[φ'.toFun ∘ UA # φ'.toFun ∘ UB] * (34 * (d[UA # UB] - dᵤ[Ax # By])) := by ring    _ = d[φ'.toFun ∘ UA # φ'.toFun ∘ UB] * (34 * (dᵤ[A # B] - dᵤ[Ax # By])) := by      rw [←  setRuzsaDist_eq_rdist hUA_unif hUB_unif hUA_mes hUB_mes]  exact (mul_le_mul_iff_right₀ h).mp this