Lax Lean Archive

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

Raw phase estimates for dependent marked units

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

    Original-rank moment tails transfer through the selected endpoint image, with a sharp target count and whole-unit marks.

    Concept map
    76 concepts; 2 descendants hidden
    100%
    Actual projected span deficitSampling after exposed coordinatesAdaptive sampling on disjoint coordinatesetsUnion over adaptive component coversExact-image bounds for independent affinecolumnsExact uniform bilinear character meanWalsh operator bounds with explicit bilinearrankRank of a lifted tensor sumIndependent binary channel charactersActual raw frame channel phase tailsJoint channel law and itsindependent-column densityActual channel moments and phase tailsCombined column and row mode exposureRows of diagonal tensor mapsMoment estimates for actual componenttensor phasesComponentwise mode spaces and diagonaltensorsExact conditioning costs and recovery offinite probability massesEntropy progress for residual pair lawsIndependence of distinct sample positionsJoin-stable classes of mode coversCount tensors killed by exposureActual exposure cover projectionRank of a diagonal familyMoments across endpoint channel groupsOriginal-rank no-cover tails for endpointgroupsDyadic span deficit estimatesA small dyadic tail scaleActual dyadic deficit recurrenceEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionProjection removes the exposed termsCount tested index occurrencesFinite linear images and their uniform-lawdensity boundsFinite even moment expansionFinite independent sampling and vertexexception tailsAmbient symmetries and frame marginalsGram-conditioned columns and theirrank-failure probabilityTwo-sided Gram normalization forindividually injective framesGreedy mode space exposureSmall actual greedy exposure tailsNo-cover rank growth on arbitrary finiteindicesActual deficits indexed by a distinct listFinite list tail statisticsFactorization and counting of low-rankbinary matricesDimension deficits after an arbitrary modemapExposed mode dimension budgetBoolean point moments with restricted basecoordinatesFinite moment probability and rank splitRaw phase estimates for dependent markedunitsA low rank sum supplies an actual adaptivecoverNo-cover phase momentsRank growth without an adaptive modecoverSquared restriction cost for independent uniteventsFinite exposure partitionsActual phase averages from small exceptionaltailsProjected nonzero terms in the actualremaining sumDimensions of projected mode spacesWalsh bounds for independent image lawsand separated phasesRank of a tensor killed in two quotientspacesRank loss under two restrictionsRaw matrix frames and their tensorrealizationThe finite uniform raw-vertex lawOriginal retained-cell laws from finite PMFsFinite relative entropy and support costsRank loss under restriction of a bilinear formImage caps inside original retained cellsOne exposure controls both modesMonotonicity of span deficitsMode space span deficitsNonzero tensor count from span deficitsRank of an actual linear map sumCharacters of all independent tensor channelsCounting component tensors with boundedtotal rankUniform raw channel phase tails overbounded-rank targetsAdmissible pair lawsOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 no_cover_marked_unit_phase proven

    2 no_cover_raw_family_tail proven

    3 no_cover_raw_phase_tail proven

    4 no_cover_uniform_target_tail proven

    Lean source view on GitHub

    1import Lax342547.DuplicatedNoCover
    2import Lax342547.PhaseAverages
    3import Lax342547.TotalRankCount
    4/-!
    5---
    6title: Raw phase estimates for dependent marked units
    7type: lemma
    8---
    9Original-rank moment tails transfer through the selected endpoint image, with a sharp target count and whole-unit marks.
    10-/
    11
    12namespace Lax342547.MultiChannelPhase
    13
    14open Lax342547.MomentSpace Lax342547.RawFrames Lax342547.ChannelDensity Lax342547.ChannelCharacters
    15open Lax342547.RealCellLaws Lax342547.FiniteSampling Lax342547.TensorCharacters
    16open Lax342547.PushforwardWalsh Lax342547.RetainedImages Lax342547.ChannelColumns
    17open Lax342547.RelativeEntropy Lax342547.ComponentSpaces Lax342547.ComponentDuals Lax342547.CoverProjection
    18open scoped BigOperators
    19
    20axiom no_cover_raw_phase_tail {e d B N Ω : Type} [Fintype e] [Fintype d] [Fintype B] [Fintype N] [Fintype Ω]
    21 [DecidableEq e] [DecidableEq d] [DecidableEq N] (E : Matrix B B Binary)
    22 (μ : Ω → ℝ) (A : Ω → e → Matrix N N Binary) (ψ : Ω → ℝ) (r h t k : ℕ) (p θ : ℝ)
    23 [Nonempty (Frame B (Fin h) N E)] (hN : 2*h+1 ≤ Fintype.card N)
    24 (hμ : Probability μ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : 1 ≤ r)
    25 (hA : ∀ x, ∑ i, (A x i).rank ≤ r) (hψ : ∀ x, |ψ x| ≤ 1)
    26 (hsize : 2*t = 2^k) (hk : 100*r+12 ≤ k) (hθ : 0 < θ)
    27 (hcover : ∀ S : Submodule Binary (e → N → Binary),
    28 ∀ T : Submodule Binary (Module.Dual Binary (e → N → Binary)),
    29 Componentwise S → DualComponentwise T →
    30 (Module.finrank Binary S : ℝ) ≤ (r : ℝ)*(2*t) →
    31 (Module.finrank Binary T : ℝ) ≤ (r : ℝ)*(2*t) →
    32 cellMass μ (fun x => projection (LinearMap.piMap (fun i => (A x i).mulVecLin)) S T = 0) ≤ p) :
    33 cellMass (weights (Lax342547.RawLaw.uniformLaw E))
    34 (fun o => θ ≤ |∑ x, μ x*ψ x*tensorCharacter h (fun i : e × d => A x i.1) (columnsEquiv h (fun a => channels (o a)))|) ≤
    35 (2 : ℝ)^(Fintype.card (e × d)*(h*h+2))*
    36 (((4 : ℝ)^(2*t)*p^(2^(k-(100*r+10)))+1/(2 : ℝ)^((Fintype.card d*h)*2^(k-(100*r+12))))/θ^(2*t))
    37
    38axiom no_cover_raw_family_tail {e d B N Ω C : Type} [Fintype e] [Fintype d] [Fintype B] [Fintype N] [Fintype Ω] [Fintype C]
    39 [DecidableEq e] [DecidableEq d] [DecidableEq N] (E : Matrix B B Binary)
    40 (μ : Ω → ℝ) (A : Ω → e → Matrix N N Binary) (ψ : C → Ω → ℝ) (r h t k : ℕ) (p θ : ℝ)
    41 [Nonempty (Frame B (Fin h) N E)] (hN : 2*h+1 ≤ Fintype.card N)
    42 (hμ : Probability μ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : 1 ≤ r)
    43 (hA : ∀ x, ∑ i, (A x i).rank ≤ r) (hψ : ∀ c x, |ψ c x| ≤ 1)
    44 (hsize : 2*t = 2^k) (hk : 100*r+12 ≤ k) (hθ : 0 < θ)
    45 (hcover : ∀ S : Submodule Binary (e → N → Binary),
    46 ∀ T : Submodule Binary (Module.Dual Binary (e → N → Binary)),
    47 Componentwise S → DualComponentwise T →
    48 (Module.finrank Binary S : ℝ) ≤ (r : ℝ)*(2*t) →
    49 (Module.finrank Binary T : ℝ) ≤ (r : ℝ)*(2*t) →
    50 cellMass μ (fun x => projection (LinearMap.piMap (fun i => (A x i).mulVecLin)) S T = 0) ≤ p) :
    51 cellMass (weights (Lax342547.RawLaw.uniformLaw E))
    52 (fun o => ∃ c : C, θ ≤ |∑ x, μ x*ψ c x*tensorCharacter h (fun i : e × d => A x i.1) (columnsEquiv h (fun a => channels (o a)))|) ≤
    53 (Fintype.card C : ℝ)*(2 : ℝ)^(Fintype.card (e × d)*(h*h+2))*
    54 (((4 : ℝ)^(2*t)*p^(2^(k-(100*r+10)))+1/(2 : ℝ)^((Fintype.card d*h)*2^(k-(100*r+12))))/θ^(2*t))
    55
    56axiom no_cover_uniform_target_tail {e d B N Ω : Type} [Fintype e] [Fintype d] [Fintype B] [Fintype N] [Fintype Ω]
    57 [DecidableEq e] [DecidableEq d] [DecidableEq N] (E : Matrix B B Binary)
    58 (μ : Ω → ℝ) (A : Ω → e → Matrix N N Binary) (ψ : (e → Matrix N N Binary) → Ω → ℝ) (r h t k : ℕ) (p θ : ℝ)
    59 [Nonempty (Frame B (Fin h) N E)] (hN : 2*h+1 ≤ Fintype.card N)
    60 (hμ : Probability μ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : 1 ≤ r)
    61 (hA : ∀ x, ∑ i, (A x i).rank ≤ r) (hψ : ∀ S, (∑ i, (S i).rank) ≤ r → ∀ x, |ψ S x| ≤ 1)
    62 (hsize : 2*t = 2^k) (hk : 100*r+12 ≤ k) (hθ : 0 < θ)
    63 (hcover : ∀ S : Submodule Binary (e → N → Binary),
    64 ∀ T : Submodule Binary (Module.Dual Binary (e → N → Binary)),
    65 Componentwise S → DualComponentwise T →
    66 (Module.finrank Binary S : ℝ) ≤ (r : ℝ)*(2*t) →
    67 (Module.finrank Binary T : ℝ) ≤ (r : ℝ)*(2*t) →
    68 cellMass μ (fun x => projection (LinearMap.piMap (fun i => (A x i).mulVecLin)) S T = 0) ≤ p) :
    69 cellMass (weights (Lax342547.RawLaw.uniformLaw E))
    70 (fun o => ∃ S : e → Matrix N N Binary, (∑ i, (S i).rank) ≤ r ∧
    71 θ ≤ |∑ x, μ x*ψ S x*tensorCharacter h (fun i : e × d => A x i.1) (columnsEquiv h (fun a => channels (o a)))|) ≤
    72 (r+1 : ℝ)^Fintype.card e*(2 : ℝ)^(2*Fintype.card N*r)*
    73 (2 : ℝ)^(Fintype.card (e × d)*(h*h+2))*
    74 (((4 : ℝ)^(2*t)*p^(2^(k-(100*r+10)))+1/(2 : ℝ)^((Fintype.card d*h)*2^(k-(100*r+12))))/θ^(2*t))
    75
    76axiom no_cover_marked_unit_phase {e d B N Ω U : Type} [Fintype e] [Fintype d] [Fintype B] [Fintype N] [Fintype Ω] [Fintype U]
    77 [DecidableEq e] [DecidableEq d] [DecidableEq N] (E : Matrix B B Binary)
    78 (μ : Ω → ℝ) (A : Ω → e → Matrix N N Binary) (ψ : (e → Matrix N N Binary) → Ω → ℝ) (r h t k : ℕ) (p θ : ℝ)
    79 [Nonempty (Frame B (Fin h) N E)] (hN : 2*h+1 ≤ Fintype.card N)
    80 (hμ : Probability μ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : 1 ≤ r)
    81 (hA : ∀ x, ∑ i, (A x i).rank ≤ r) (hψ : ∀ S, (∑ i, (S i).rank) ≤ r → ∀ x, |ψ S x| ≤ 1)
    82 (hsize : 2*t = 2^k) (hk : 100*r+12 ≤ k) (hθ : 0 < θ)
    83 (β : U → ℝ) (image : U → (e × d) → Frame B (Fin h) N E) (L : ℝ)
    84 (S : U → e → Matrix N N Binary)
    85 (hβ : Probability β) (hL : 0 ≤ L)
    86 (hβcap : ∀ o, push β image o ≤ L*weights (Lax342547.RawLaw.uniformLaw E) o)
    87 (hS : ∀ o, (∑ i, (S o i).rank) ≤ r)
    88 (hcover : ∀ S : Submodule Binary (e → N → Binary),
    89 ∀ T : Submodule Binary (Module.Dual Binary (e → N → Binary)),
    90 Componentwise S → DualComponentwise T →
    91 (Module.finrank Binary S : ℝ) ≤ (r : ℝ)*(2*t) →
    92 (Module.finrank Binary T : ℝ) ≤ (r : ℝ)*(2*t) →
    93 cellMass μ (fun x => projection (LinearMap.piMap (fun i => (A x i).mulVecLin)) S T = 0) ≤ p) :
    94 |∑ o, β o*(∑ x, μ x*ψ (S o) x*tensorCharacter h (fun i : e × d => A x i.1) (columnsEquiv h (fun a => channels (image o a))))| ≤
    95 θ+L*((r+1 : ℝ)^Fintype.card e*(2 : ℝ)^(2*Fintype.card N*r)*
    96 (2 : ℝ)^(Fintype.card (e × d)*(h*h+2))*
    97 (((4 : ℝ)^(2*t)*p^(2^(k-(100*r+10)))+1/(2 : ℝ)^((Fintype.card d*h)*2^(k-(100*r+12))))/θ^(2*t)))
    98
    99end Lax342547.MultiChannelPhase
    100
    Show ProofShow ProofShow ProofShow 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…