Lax Lean Archive

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

Original retained-cell laws from finite PMFs

Lax342547.RealCellLaws · concepts/Lax342547/RealCellLaws.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

    Finite PMF events convert to real weights and normalized laws supported on the original retained cell. Joint image caps yield the paper conditional exponent without intersecting or changing that cell.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 10 statements. Each proof establishes one of them relative to its assumptions.

    1 event_mass proven

    2 pmf_paper_subtype_cap proven

    3 pmf_subtype_conditional_cap proven

    4 subtype_conditional_cap proven

    5 subtype_image_push proven

    6 subtype_integral proven

    7 subtype_weights_nonneg proven

    8 subtype_weights_total proven

    9 weights_nonneg proven

    10 weights_total proven

    Lean source view on GitHub

    1import Lax342547.RetainedImages
    2import Lax342547.Conditioning
    3import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
    4
    5/-!
    6---
    7title: Original retained-cell laws from finite PMFs
    8type: lemma
    9---
    10Finite PMF events convert to real weights and normalized laws supported on the original retained cell. Joint image caps yield the paper conditional exponent without intersecting or changing that cell.
    11-/
    12
    13namespace Lax342547.RealCellLaws
    14
    15open Lax342547.RetainedImages Lax342547.PushforwardWalsh
    16open scoped ENNReal
    17
    18noncomputable def weights {Ω : Type} (p : PMF Ω) : Ω → ℝ := fun ω => (p ω).toReal
    19
    20axiom weights_nonneg {Ω : Type} (p : PMF Ω) (ω : Ω) : 0 ≤ weights p ω
    21
    22axiom weights_total {Ω : Type} [Fintype Ω] (p : PMF Ω) : ∑ ω, weights p ω = 1
    23
    24axiom event_mass {Ω : Type} [Fintype Ω] (p : PMF Ω) (C : Ω → Prop) :
    25 cellMass (weights p) C = (p.toOuterMeasure {ω | C ω}).toReal
    26
    27noncomputable def subtypeWeights {Ω : Type} [Fintype Ω] (ρ : Ω → ℝ) (C : Ω → Prop) :
    28 {ω // C ω} → ℝ := fun ω => ρ ω.val / cellMass ρ C
    29
    30axiom subtype_integral {Ω : Type} [Fintype Ω]
    31 (ρ : Ω → ℝ) (C : Ω → Prop) (f : Ω → ℝ) : by
    32 classical
    33 exact (∑ ω : {ω // C ω}, subtypeWeights ρ C ω * f ω.val) =
    34 ∑ ω, conditionalLaw ρ C ω * f ω
    35
    36axiom subtype_weights_total {Ω : Type} [Fintype Ω]
    37 (ρ : Ω → ℝ) (C : Ω → Prop) (hC : 0 < cellMass ρ C) : by
    38 classical
    39 exact (∑ ω : {ω // C ω}, subtypeWeights ρ C ω) = 1
    40
    41axiom subtype_weights_nonneg {Ω : Type} [Fintype Ω]
    42 (ρ : Ω → ℝ) (C : Ω → Prop) (hρ : ∀ ω, 0 ≤ ρ ω) (hC : 0 < cellMass ρ C)
    43 (ω : {ω // C ω}) : 0 ≤ subtypeWeights ρ C ω
    44
    45axiom subtype_image_push {Ω X : Type} [Fintype Ω]
    46 (ρ : Ω → ℝ) (C : Ω → Prop) (image : Ω → X) (x : X) : by
    47 classical
    48 exact push (subtypeWeights ρ C) (fun ω => image ω.val) x = push (conditionalLaw ρ C) image x
    49
    50axiom subtype_conditional_cap {Ω X : Type} [Fintype Ω]
    51 (ρ : Ω → ℝ) (C : Ω → Prop) (image : Ω → X) (joint : Ω → Prop)
    52 (τ cap : ℝ) (hρ : ∀ ω, 0 ≤ ρ ω) (hτ : 0 < τ)
    53 (hC : τ ≤ cellMass ρ C) (hCJ : ∀ ω, C ω → joint ω)
    54 (hcap : ∀ x, cellMass ρ (fun ω => joint ω ∧ image ω = x) ≤ cap) (x : X) : by
    55 classical
    56 exact push (subtypeWeights ρ C) (fun ω => image ω.val) x ≤ cap / τ
    57
    58axiom pmf_subtype_conditional_cap {Ω X : Type} [Fintype Ω]
    59 (p : PMF Ω) (C : Ω → Prop) (image : Ω → X) (joint : Ω → Prop)
    60 (τ : ℝ) (cap : ℝ≥0∞) (hcapTop : cap ≠ ⊤) (hτ : 0 < τ)
    61 (hC : τ ≤ (p.toOuterMeasure {ω | C ω}).toReal) (hCJ : ∀ ω, C ω → joint ω)
    62 (hcap : ∀ x, p.toOuterMeasure {ω | joint ω ∧ image ω = x} ≤ cap) (x : X) : by
    63 classical
    64 exact push (subtypeWeights (weights p) C) (fun ω => image ω.val) x ≤ cap.toReal / τ
    65
    66axiom pmf_paper_subtype_cap {Ω X : Type} [Fintype Ω]
    67 (p : PMF Ω) (C : Ω → Prop) (image : Ω → X) (joint : Ω → Prop)
    68 (ζ k t N : ℝ) (hζ : 0 ≤ ζ) (hζsmall : ζ ≤ 1 / 1000)
    69 (hk : 2 * ζ * k ≤ 1 / 500) (ht : 1 ≤ t) (hN : 0 ≤ N)
    70 (hC : (2 : ℝ) ^ (-(k + 1 / 100) * N) ≤ (p.toOuterMeasure {ω | C ω}).toReal)
    71 (hCJ : ∀ ω, C ω → joint ω)
    72 (hcap : ∀ x, p.toOuterMeasure {ω | joint ω ∧ image ω = x} ≤
    73 (2 : ℝ≥0∞) ^ (-(1 - 2 * ζ) * (k + t) * N)) (x : X) : by
    74 classical
    75 exact push (subtypeWeights (weights p) C) (fun ω => image ω.val) x ≤
    76 (2 : ℝ) ^ (-(95 / 100 : ℝ) * t * N)
    77
    78end Lax342547.RealCellLaws
    79
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…