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

entropic_PFR_conjecture'

PFR.EntropyPFR · PFR/EntropyPFR.lean:69 to 80

Mathematical statement

Exact Lean statement

theorem entropic_PFR_conjecture' (hpη : p.η = 1 / 9) :
    ∃ H : Submodule (ZMod 2) G, ∃ Ω : Type uG, ∃ mΩ : MeasureSpace Ω, ∃ U : Ω → G,
    IsUniform H U ∧ d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧
      d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem entropic_PFR_conjecture' (hpη : p.η = 1 / 9) :    ∃ H : Submodule (ZMod 2) G, ∃ Ω : Type uG, ∃ mΩ : MeasureSpace Ω, ∃ U : Ω → G,    IsUniform H U ∧ d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧      d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] := by  have : d[p.X₀₁ # p.X₀₂] = d[p.X₀₂ # p.X₀₁] := rdist_symm  obtain ⟨H, Ω, mΩ, U, H', hU, hUnif, h'⟩ := entropic_PFR_conjecture p hpη  refine ⟨H, Ω, mΩ, U, hUnif, ?_⟩  have : d[p.X₀₁ # U] ≤ d[p.X₀₁ # p.X₀₂] + d[p.X₀₂ # U] := rdist_triangle p.hmeas1 p.hmeas2 hU  have : d[p.X₀₂ # U] ≤ d[p.X₀₂ # p.X₀₁] + d[p.X₀₁ # U] := rdist_triangle p.hmeas2 p.hmeas1 hU  constructor  · linarith  · linarith