Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Joint fresh-image entropy on original retained leaf cells

Lax342547.LeafCellImages · concepts/Lax342547/LeafCellImages.lean · lax-342547

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Exact all-rank leaf caps combine known key directions with fresh directions. Conditioning on the original retained cell gives the paper .95 rank exponent, for tuples of arbitrary rank.

    Concept map
    12 concepts; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax342547.JointKeyCap
    2import Lax342547.RealCellLaws
    3
    4/-!
    5---
    6title: Joint fresh-image entropy on original retained leaf cells
    7type: lemma
    8---
    9Exact all-rank leaf caps combine known key directions with fresh directions. Conditioning on the original retained cell gives the paper .95 rank exponent, for tuples of arbitrary rank.
    10-/
    11
    12namespace Lax342547.LeafCellImages
    13
    14open Lax342547.MomentSpace Lax342547.ExactPins
    15open Lax342547.RealCellLaws Lax342547.RetainedImages Lax342547.PushforwardWalsh
    16open scoped ENNReal
    17
    18noncomputable def freshImage {Ω Axis I N : Type} {V : Axis → Type}
    19 [∀ a, AddCommGroup (V a)] [∀ a, Module Binary (V a)]
    20 (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
    21 (fresh : ∀ a, V a →ₗ[Binary] (I → Binary))
    22 (ω : Ω) : ∀ a, V a →ₗ[Binary] (N → Binary) := fun a => (A ω a).comp (fresh a)
    23
    24axiom original_leaf_cell_image_cap {Ω Axis I N : Type} {U V : Axis → Type}
    25 [Fintype Ω] [Fintype Axis] [Fintype I] [Fintype N]
    26 [∀ a, AddCommGroup (U a)] [∀ a, Module Binary (U a)] [∀ a, FiniteDimensional Binary (U a)]
    27 [∀ a, AddCommGroup (V a)] [∀ a, Module Binary (V a)] [∀ a, FiniteDimensional Binary (V a)]
    28 (p : PMF Ω) (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
    29 (P : Pin Axis I N) (keys : ∀ a, U a →ₗ[Binary] (I → Binary))
    30 (fresh : ∀ a, V a →ₗ[Binary] (I → Binary))
    31 (hkeys : ∀ a, Function.Injective ((P.space a).mkQ.comp (keys a)))
    32 (hfresh : ∀ a, Function.Injective (((P.space a) ⊔ LinearMap.range (keys a)).mkQ.comp (fresh a)))
    33 (yk : ∀ a, U a →ₗ[Binary] (N → Binary)) (C : Ω → Prop)
    34 (hCkey : ∀ ω, C ω → ∀ a, (A ω a).comp (keys a) = yk a)
    35 (ζ : ℝ) (hζ : 0 ≤ ζ) (hζsmall : ζ ≤ 1 / 1000)
    36 (hk : 2 * ζ * (∑ a, Module.finrank Binary (U a)) ≤ (1 / 500 : ℝ))
    37 (ht : 1 ≤ ∑ a, Module.finrank Binary (V a))
    38 (hC : (2 : ℝ)^(-(((∑ a, Module.finrank Binary (U a) : ℕ) : ℝ) + 1 / 100) * Fintype.card N) ≤
    39 (p.toOuterMeasure {ω | C ω}).toReal)
    40 (hcap : ∀ Q : Pin Axis I N, 1 ≤ P.relativeRank Q →
    41 p.toOuterMeasure (Q.event A) ≤
    42 ((2 : ℝ≥0∞)^(-(1 - 2 * ζ) * Fintype.card N)) ^ (P.relativeRank Q))
    43 (y : ∀ a, V a →ₗ[Binary] (N → Binary)) : by
    44 classical
    45 exact push (subtypeWeights (weights p) C) (fun ω => freshImage A fresh ω.val) y ≤
    46 (2 : ℝ)^(-(95/100 : ℝ)*(∑ a, Module.finrank Binary (V a))*Fintype.card N)
    47
    48end Lax342547.LeafCellImages
    49
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…