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

PFR_projection

PFR.WeakPFR · PFR/WeakPFR.lean:389 to 399

Source documentation

If $G=\mathbb{F}_2^d$ and X, Y are G-valued random variables then there is a subgroup $H\leq \mathbb{F}_2^d$ such that [\log \lvert H\rvert \leq 2 * (\mathbb{H}(X)+\mathbb{H}(Y))] and if $\psi:G \to G/H$ is the natural projection then [\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 34 * d[\psi(X);\psi(Y)].]

Exact Lean statement

lemma PFR_projection (hX : Measurable X) (hY : Measurable Y) :
    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) ≤ 2 * (H[X; μ] + H[Y;μ']) ∧
    H[H.mkQ ∘ X; μ] + H[H.mkQ ∘ Y; μ'] ≤
      34 * d[H.mkQ ∘ X;μ # H.mkQ ∘ Y;μ']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma PFR_projection (hX : Measurable X) (hY : Measurable Y) :    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) ≤ 2 * (H[X; μ] + H[Y;μ']) ∧    H[H.mkQ ∘ X; μ] + H[H.mkQ ∘ Y; μ'] ≤      34 * d[H.mkQ ∘ X;μ # H.mkQ ∘ Y;μ'] := by  rcases PFR_projection' X Y μ μ' ((3 : ℝ) / 5) hX hY (by norm_num) (by norm_num) with ⟨H, h, h'⟩  refine ⟨H, ?_, ?_⟩  · convert h    norm_num  · have : 0 ≤ d[⇑H.mkQ ∘ X; μ # ⇑H.mkQ ∘ Y; μ'] :=      rdist_nonneg (.comp .of_discrete hX) (.comp .of_discrete hY)    linarith