PFR_projection'

lemma PFR_projection'    (α : ℝ) (hX : Measurable X) (hY : Measurable Y) (αpos : 0 < α) (αone : α < 1) :    ∃ H : Submodule (ZMod 2) G,      log (Nat.card H) ≤ (1 + α) / (2 * (1 - α)) * (H[X; μ] + H[Y; μ']) ∧        α * (H[H.mkQ ∘ X; μ] + H[H.mkQ ∘ Y; μ']) ≤ 20 * d[H.mkQ ∘ X; μ # H.mkQ ∘ Y; μ'] := by  let S := {H : Submodule (ZMod 2) G | (∃ (c : ℝ), 0 ≤ c ∧      log (Nat.card H) ≤ (1 + α) / (2 * (1 - α)) * (1 - c) * (H[X; μ] + H[Y;μ']) ∧    H[H.mkQ ∘ X; μ] + H[H.mkQ ∘ Y; μ'] ≤ c * (H[X; μ] + H[Y;μ'])) ∧    20 * d[H.mkQ ∘ X; μ # H.mkQ ∘ Y; μ'] < α * (H[H.mkQ ∘ X; μ ] + H[H.mkQ ∘ Y; μ'])}  have : 0 ≤ H[X; μ] + H[Y; μ'] := by linarith [entropy_nonneg X μ, entropy_nonneg Y μ']  have : 0 < 1 - α := sub_pos.mpr αone  by_cases hE : ⊥ ∈ S  · classical    obtain ⟨H, ⟨⟨c, hc, hlog, hup⟩, hent⟩, hMaxl⟩ :=      S.toFinite.exists_maximal (Set.nonempty_of_mem hE)    set G' := G ⧸ H    set ψ : G →ₗ[ZMod 2] G' := H.mkQ    have surj : Function.Surjective ψ := Submodule.Quotient.mk_surjective H    obtain ⟨H', hlog', hup'⟩ := app_ent_PFR _ _ _ _ α hent (.comp .of_discrete hX)      (.comp .of_discrete hY)    have H_ne_bot : H' ≠ ⊥ := by      by_contra!      rcases this with rfl      have inj : Function.Injective (Submodule.mkQ (⊥ : Submodule (ZMod 2) G')) :=        QuotientAddGroup.quotientBot.symm.injective      rw [entropy_comp_of_injective _ (.comp .of_discrete hX) _ inj,          entropy_comp_of_injective _ (.comp .of_discrete hY) _ inj] at hup'      nlinarith [entropy_nonneg (ψ ∘ X) μ, entropy_nonneg (ψ ∘ Y) μ']    let H'' := H'.comap ψ    use H''    rw [← (Submodule.map_comap_eq_of_surjective surj _ : H''.map ψ = H')] at hup' hlog'    set H' := H''.map ψ    have Hlt :=      calc        H = (⊥ : Submodule (ZMod 2) G').comap ψ := by simp [ψ]; rw [Submodule.ker_mkQ]        _ < H'' := by rw [Submodule.comap_lt_comap_iff_of_surjective surj]; exact H_ne_bot.bot_lt    let φ : (G' ⧸ H') ≃ₗ[ZMod 2] (G ⧸ H'') := Submodule.quotientQuotientEquivQuotient H H'' Hlt.le    set ψ' : G' →ₗ[ZMod 2] G' ⧸ H' := H'.mkQ    set ψ'' : G →ₗ[ZMod 2] G ⧸ H'' := H''.mkQ    have diag : ψ' ∘ ψ = φ.symm ∘ ψ'' := rfl    rw [← Function.comp_assoc, ← Function.comp_assoc, diag, Function.comp_assoc,        Function.comp_assoc] at hup'    have cond : log (Nat.card H'') ≤        (1 + α) / (2 * (1 - α)) * (1 - α * c) * (H[X; μ] + H[Y;μ']) := by      have cardprod : Nat.card H'' = Nat.card H' * Nat.card H := by        have hcard₀ := Nat.card_congr <| (Submodule.comapSubtypeEquivOfLe Hlt.le).toEquiv        have hcard₁ := Nat.card_congr <| (ψ.domRestrict H'').quotKerEquivRange.toEquiv        have hcard₂ := (H.comap H''.subtype).card_eq_card_quotient_mul_card        rw [ψ.ker_domRestrict H'', Submodule.ker_mkQ, ψ.range_domRestrict H''] at hcard₁        simpa only [← Nat.card_eq_fintype_card, hcard₀, hcard₁, mul_comm] using hcard₂      calc          log (Nat.card H'')      _ = log (Nat.card H' * Nat.card H) := by rw [cardprod]; norm_cast      _ = log (Nat.card H') + log (Nat.card H) := by        rw [Real.log_mul (Nat.cast_ne_zero.2 (@Nat.card_pos H').ne')              (Nat.cast_ne_zero.2 (@Nat.card_pos H).ne')]      _ ≤ (1 + α) / 2 * (H[ψ ∘ X; μ] + H[ψ ∘ Y; μ']) + log (Nat.card H) := by gcongr      _ ≤ (1 + α) / 2 * (c * (H[X; μ] + H[Y;μ'])) +            (1 + α) / (2 * (1 - α)) * (1 - c) * (H[X; μ] + H[Y; μ']) := by gcongr      _ = (1 + α) / (2 * (1 - α)) * (1 - α * c) * (H[X; μ] + H[Y; μ']) := by        field_simp; ring    have HS : H'' ∉ S := fun Hs => Hlt.not_ge (hMaxl Hs Hlt.le)    simp only [S, Set.mem_setOf_eq, not_and, not_lt] at HS    refine ⟨?_, HS ⟨α * c, by positivity, cond, ?_⟩⟩    · calc      log (Nat.card H'')      _ ≤ (1 + α) / (2 * (1 - α)) * (1 - α * c) * (H[X; μ] + H[Y;μ']) := cond      _ ≤ (1 + α) / (2 * (1 - α)) * 1 * (H[X; μ] + H[Y;μ']) := by gcongr; simp; positivity      _ = (1 + α) / (2 * (1 - α)) * (H[X; μ] + H[Y;μ']) := by simp only [mul_one]    · calc      H[ψ'' ∘ X; μ ] + H[ψ'' ∘ Y; μ' ]      _ = H[φ.symm ∘ ψ'' ∘ X; μ ] + H[φ.symm ∘ ψ'' ∘ Y; μ' ] := by        simp_rw [← entropy_comp_of_injective _ (.comp .of_discrete hX) _ φ.symm.injective,                 ← entropy_comp_of_injective _ (.comp .of_discrete hY) _ φ.symm.injective]      _ ≤ α * (H[ψ ∘ X; μ ] + H[ψ ∘ Y; μ' ]) := hup'.le      _ ≤ α * (c * (H[X; μ] + H[Y; μ'])) := by gcongr      _ = (α * c) * (H[X; μ] + H[Y; μ']) := by ring  · refine ⟨⊥, ?_, ?_⟩    · simp only [Nat.card_eq_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one, log_one]      positivity    · simp only [S, Set.mem_setOf_eq, not_and, not_lt] at hE      exact hE ⟨1, by norm_num, by        norm_num; exact add_le_add (entropy_comp_le μ hX _) (entropy_comp_le μ' hY _)⟩