Joint matrix-image caps for retained leaf laws
Lax342547.LeafBlockCaps · concepts/Lax342547/LeafBlockCaps.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
Joint fresh linear images flatten to the rank-factor matrix tuples used by Walsh characters. Exact leaf caps give all-rank component image bounds on original retained cells, including the rank-zero normalization case.
Concept map
Evidence
This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.
1 block_image_fiber proven
2 block_image_push proven
3 original_leaf_all_rank_block_cap proven
4 original_leaf_block_cap proven
Lean source view on GitHub
| 1 | import Lax342547.LeafCellImages |
| 2 | import Lax342547.ComponentCharacters |
| 3 | import Lax342547.PairedFrames |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Joint matrix-image caps for retained leaf laws |
| 8 | type: lemma |
| 9 | --- |
| 10 | Joint fresh linear images flatten to the rank-factor matrix tuples used by Walsh characters. Exact leaf caps give all-rank component image bounds on original retained cells, including the rank-zero normalization case. |
| 11 | -/ |
| 12 | |
| 13 | namespace Lax342547.LeafBlockCaps |
| 14 | |
| 15 | open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.PushforwardWalsh |
| 16 | open Lax342547.RealCellLaws Lax342547.LeafCellImages Lax342547.ComponentCharacters |
| 17 | open Lax342547.CoefficientPhase |
| 18 | open scoped ENNReal |
| 19 | |
| 20 | noncomputable def decodedImages {Axis N : Type} {R : Axis → Type} [∀ _a, Fintype (R _a)] |
| 21 | (y : ((Σ a, R a) × N) → Binary) : ∀ a, (R a → Binary) →ₗ[Binary] (N → Binary) := |
| 22 | fun a => Matrix.mulVecLin (fun n i => y (⟨a,i⟩,n)) |
| 23 | |
| 24 | axiom block_image_fiber {Axis I N : Type} {R : Axis → Type} |
| 25 | [Fintype I] [Fintype N] [∀ _a, Fintype (R _a)] |
| 26 | (F : ∀ a, Matrix I (R a) Binary) (X : ∀ _a, Matrix N I Binary) |
| 27 | (y : ((Σ a, R a) × N) → Binary) : by |
| 28 | classical |
| 29 | exact blockImage F X = y ↔ ∀ a, (X a).mulVecLin.comp (F a).mulVecLin = decodedImages y a |
| 30 | |
| 31 | axiom block_image_push {Ω Axis I N : Type} {R : Axis → Type} |
| 32 | [Fintype Ω] [Fintype I] [Fintype N] [∀ _a, Fintype (R _a)] |
| 33 | (ρ : Ω → ℝ) (F : ∀ a, Matrix I (R a) Binary) (X : Ω → ∀ _a, Matrix N I Binary) |
| 34 | (y : ((Σ a, R a) × N) → Binary) : by |
| 35 | classical |
| 36 | exact push ρ (fun ω => blockImage F (X ω)) y = |
| 37 | push ρ (freshImage (fun ω a => (X ω a).mulVecLin) (fun a => (F a).mulVecLin)) |
| 38 | (decodedImages y) |
| 39 | |
| 40 | axiom original_leaf_block_cap {Ω Axis I N : Type} {U : Axis → Type} |
| 41 | [Fintype Ω] [Fintype Axis] [Fintype I] [Fintype N] |
| 42 | [∀ a, AddCommGroup (U a)] [∀ a, Module Binary (U a)] [∀ a, FiniteDimensional Binary (U a)] |
| 43 | (p : PMF Ω) (X : Ω → Axis → Matrix N I Binary) |
| 44 | (P : Pin Axis I N) (keys : ∀ a, U a →ₗ[Binary] (I → Binary)) |
| 45 | (r : Axis → ℕ) (F : ∀ a, Matrix I (Fin (r a)) Binary) |
| 46 | (hkeys : ∀ a, Function.Injective ((P.space a).mkQ.comp (keys a))) |
| 47 | (hfresh : ∀ a, Function.Injective (((P.space a) ⊔ LinearMap.range (keys a)).mkQ.comp (F a).mulVecLin)) |
| 48 | (yk : ∀ a, U a →ₗ[Binary] (N → Binary)) (C : Ω → Prop) |
| 49 | (hCkey : ∀ ω, C ω → ∀ a, (X ω a).mulVecLin.comp (keys a) = yk a) |
| 50 | (ζ : ℝ) (hζ : 0 ≤ ζ) (hζsmall : ζ ≤ 1 / 1000) |
| 51 | (hk : 2 * ζ * (∑ a, Module.finrank Binary (U a)) ≤ (1 / 500 : ℝ)) |
| 52 | (ht : 1 ≤ ∑ a, r a) |
| 53 | (hC : (2 : ℝ)^(-(((∑ a, Module.finrank Binary (U a) : ℕ) : ℝ) + 1 / 100) * Fintype.card N) ≤ |
| 54 | (p.toOuterMeasure {ω | C ω}).toReal) |
| 55 | (hcap : ∀ Q : Pin Axis I N, 1 ≤ P.relativeRank Q → |
| 56 | p.toOuterMeasure (Q.event (fun ω a => (X ω a).mulVecLin)) ≤ |
| 57 | ((2 : ℝ≥0∞)^(-(1 - 2 * ζ) * Fintype.card N)) ^ (P.relativeRank Q)) |
| 58 | (y : ((Σ a, Fin (r a)) × N) → Binary) : by |
| 59 | classical |
| 60 | exact push (subtypeWeights (weights p) C) (fun ω => blockImage F (X ω.val)) y ≤ |
| 61 | (2 : ℝ)^(-(95/100 : ℝ)*(∑ a, r a)*Fintype.card N) |
| 62 | |
| 63 | axiom original_leaf_all_rank_block_cap {Ω Axis I N : Type} {U : Axis → Type} |
| 64 | [Fintype Ω] [Fintype Axis] [Fintype I] [Fintype N] |
| 65 | [∀ a, AddCommGroup (U a)] [∀ a, Module Binary (U a)] [∀ a, FiniteDimensional Binary (U a)] |
| 66 | (p : PMF Ω) (X : Ω → Axis → Matrix N I Binary) |
| 67 | (P : Pin Axis I N) (keys : ∀ a, U a →ₗ[Binary] (I → Binary)) |
| 68 | (r : Axis → ℕ) (F : ∀ a, Matrix I (Fin (r a)) Binary) |
| 69 | (hkeys : ∀ a, Function.Injective ((P.space a).mkQ.comp (keys a))) |
| 70 | (hfresh : ∀ a, Function.Injective (((P.space a) ⊔ LinearMap.range (keys a)).mkQ.comp (F a).mulVecLin)) |
| 71 | (yk : ∀ a, U a →ₗ[Binary] (N → Binary)) (C : Ω → Prop) |
| 72 | (hCkey : ∀ ω, C ω → ∀ a, (X ω a).mulVecLin.comp (keys a) = yk a) |
| 73 | (ζ : ℝ) (hζ : 0 ≤ ζ) (hζsmall : ζ ≤ 1 / 1000) |
| 74 | (hk : 2 * ζ * (∑ a, Module.finrank Binary (U a)) ≤ (1 / 500 : ℝ)) |
| 75 | (hC : (2 : ℝ)^(-(((∑ a, Module.finrank Binary (U a) : ℕ) : ℝ) + 1 / 100) * Fintype.card N) ≤ |
| 76 | (p.toOuterMeasure {ω | C ω}).toReal) |
| 77 | (hcap : ∀ Q : Pin Axis I N, 1 ≤ P.relativeRank Q → |
| 78 | p.toOuterMeasure (Q.event (fun ω a => (X ω a).mulVecLin)) ≤ |
| 79 | ((2 : ℝ≥0∞)^(-(1 - 2 * ζ) * Fintype.card N)) ^ (P.relativeRank Q)) |
| 80 | (y : ((Σ a, Fin (r a)) × N) → Binary) : by |
| 81 | classical |
| 82 | exact push (subtypeWeights (weights p) C) (fun ω => blockImage F (X ω.val)) y ≤ |
| 83 | (2 : ℝ)^(-(95/100 : ℝ)*(∑ a, r a)*Fintype.card N) |
| 84 | |
| 85 | end Lax342547.LeafBlockCaps |
| 86 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments