Source indexedlemma · leanprover/lean4:v4.33.0-rc1

app_ent_PFR'

PFR.WeakPFR · PFR/WeakPFR.lean:241 to 282

Source documentation

Let $G=\mathbb{F}_2^n$ and X, Y be G-valued random variables such that [\mathbb{H}(X)+\mathbb{H}(Y)> (20/\alpha) d[X;Y],] for some $\alpha > 0$ . There is a non-trivial subgroup $H\leq G$ such that [\log \lvert H\rvert <(1+\alpha)/2 (\mathbb{H}(X)+\mathbb{H}(Y))] and [\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))< \alpha (\mathbb{H}(X)+\mathbb{H}(Y))] where $\psi:G\to G/H$ is the natural projection homomorphism.

Exact Lean statement

lemma app_ent_PFR' [mΩ : MeasureSpace Ω] [mΩ' : MeasureSpace Ω'] (X : Ω → G) (Y : Ω' → G)
    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]
    {α : ℝ} (hent : 20 * d[X # Y] < α * (H[X] + H[Y])) (hX : Measurable X) (hY : Measurable Y) :
    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) < (1 + α) / 2 * (H[X] + H[Y]) ∧
      H[H.mkQ ∘ X] + H[H.mkQ ∘ Y] < α * (H[X] + H[Y])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma app_ent_PFR' [mΩ : MeasureSpace Ω] [mΩ' : MeasureSpace Ω'] (X : Ω → G) (Y : Ω' → G)    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]    {α : ℝ} (hent : 20 * d[X # Y] < α * (H[X] + H[Y])) (hX : Measurable X) (hY : Measurable Y) :    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) < (1 + α) / 2 * (H[X] + H[Y]) ∧      H[H.mkQ ∘ X] + H[H.mkQ ∘ Y] < α * (H[X] + H[Y]) := by  let p : refPackage Ω Ω' G := {    X₀₁ := X    X₀₂ := Y    hmeas1 := hX    hmeas2 := hY    η := 1/8    hη := by norm_num    hη' := by norm_num }  obtain ⟨H, Ω'', hΩ'', U, _, hUmeas, hUunif, ineq⟩ := entropic_PFR_conjecture_improv p rfl  let ψ := H.mkQ  use H  have H_fin : Finite H := Subtype.finite  -- Note that H[ψ ∘ X] + H[ψ ∘ Y] ≤ 20 * d[X # Y]  have ent_le : H[ψ ∘ X] + H[ψ ∘ Y] ≤ 20 * d[X # Y] := calc    H[ψ ∘ X] + H[ψ ∘ Y] ≤ 2 * d[X # U] + 2 * d[Y # U] := by      gcongr      · exact ent_of_proj_le hX hUmeas H_fin hUunif      · exact ent_of_proj_le hY hUmeas H_fin hUunif    _ = 2 * (d[X # U] + d[Y # U]) := by ring    _ ≤ 2 * (10 * d[X # Y]) := by gcongr    _ = 20 * d[X # Y] := by ring  -- Note that (log (Nat.card H) - H[X]) + (log (Nat.card H) - H[Y]) ≤ 20 * d[X # Y]  have log_sub_le : (log (Nat.card H) - H[X]) + (log (Nat.card H) - H[Y]) ≤ 20 * d[X # Y] := calc    (log (Nat.card H) - H[X]) + (log (Nat.card H) - H[Y]) =      (H[U] - H[X]) + (H[U] - H[Y]) := by        rw [IsUniform.entropy_eq' H_fin hUunif hUmeas]        norm_cast    _ ≤ |(H[U] - H[X])| + |(H[U] - H[Y])| := by gcongr <;> exact le_abs_self _    _ ≤ 2 * d[X # U] + 2 * d[Y # U] := by      gcongr      · rw [rdist_symm]; exact diff_ent_le_rdist hUmeas hX      · rw [rdist_symm]; exact diff_ent_le_rdist hUmeas hY    _ = 2 * (d[X # U] + d[Y # U]) := by ring    _ ≤ 2 * (10 * d[X # Y]) := by gcongr    _ = 20 * d[X # Y] := by ring  -- then the conclusion follows from the assumption `hent` and basic inequality manipulations  exact ⟨by linarith, by linarith⟩