BanditRLProof.LowerBounds.SuccinctGeometryAudit

Source Axiom 3.1: a nonempty collection of unit atoms closed under negation. No spanning assumption is added.

structure SuccinctUnitSystem (V : Type*) [NormedAddCommGroup V] [InnerProductSpace ℝ V] where

The source quantity `Q(X)=sup_{E in U} <X,E>`.

def sourceQ (system : SuccinctUnitSystem V) (x : V) : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQSet_bddAbove (system : SuccinctUnitSystem V) (x : V) : BddAbove ((fun e : V => ⟪x, e⟫_ℝ) '' system.atoms)

No declaration docstring is present; use the chapter context and exact statement below.

theorem le_sourceQ_of_mem (system : SuccinctUnitSystem V) {x e : V} (he : e ∈ system.atoms) : ⟪x, e⟫_ℝ ≤ system.sourceQ x

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQ_le_norm (system : SuccinctUnitSystem V) (x : V) : system.sourceQ x ≤ ‖x‖

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQ_nonneg (system : SuccinctUnitSystem V) (x : V) : 0 ≤ system.sourceQ x

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQ_zero (system : SuccinctUnitSystem V) : system.sourceQ 0 = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem abs_inner_le_sourceQ_of_mem (system : SuccinctUnitSystem V) {x e : V} (he : e ∈ system.atoms) : |⟪x, e⟫_ℝ| ≤ system.sourceQ x

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQ_eq_zero_of_atom_orthogonal (system : SuccinctUnitSystem V) {x : V} (horthogonal : ∀ e ∈ system.atoms, ⟪x, e⟫_ℝ = 0) : system.sourceQ x = 0

The source quantity `R(X)=sup_{Q(Y)<=1} <X,Y>`, retained as a real-valued `sSup`. Consumers must separately prove the defining set is bounded.

def sourceR (system : SuccinctUnitSystem V) (x : V) : ℝ

If a nonzero ambient direction is orthogonal to every atom, the set used to define its source `R` is unbounded. This exposes the hidden global regularity/codomain obligation in Definition 3.2.

theorem sourceRSet_not_bddAbove_of_nonzero_atom_orthogonal (system : SuccinctUnitSystem V) {x : V} (hx : x ≠ 0) (horthogonal : ∀ e ∈ system.atoms, ⟪x, e⟫_ℝ = 0) : ¬ BddAbove ((fun y : V => ⟪x, y⟫_ℝ) '' {y | system.sourceQ y ≤ 1})

Source Definition 3.1. The explicit boundedness field is the ordinary mathematical meaning of the displayed finite real supremum, not a replacement for the source equality.

structure IsSuccinctSupport (system : SuccinctUnitSystem V) {s : Nat} (basis : Fin s → V) : Prop where

No declaration docstring is present; use the chapter context and exact statement below.

theorem correlationSum_le_one (support : IsSuccinctSupport system basis) {e : V} (he : e ∈ system.atoms) : (∑ i, |⟪e, basis i⟫_ℝ|) ≤ 1

The mutual-orthogonality consequence stated after source Definition 3.1.

theorem inner_basis_basis (support : IsSuccinctSupport system basis) (i j : Fin s) : ⟪basis i, basis j⟫_ℝ = if i = j then 1 else 0

A source succinct support is an orthonormal family. This is the Mathlib interface consumed by the finite Bessel step in source Lemma 3.3.

theorem orthonormal (support : IsSuccinctSupport system basis) : Orthonormal ℝ basis

The finite maximum appearing in source Lemma 3.1.

def maxAbsCoefficient [Nonempty (Fin s)] (a : Fin s → ℝ) : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem abs_le_maxAbsCoefficient [Nonempty (Fin s)] (a : Fin s → ℝ) (i : Fin s) : |a i| ≤ maxAbsCoefficient a

No declaration docstring is present; use the chapter context and exact statement below.

theorem maxAbsCoefficient_nonneg [Nonempty (Fin s)] (a : Fin s → ℝ) : 0 ≤ maxAbsCoefficient a

No declaration docstring is present; use the chapter context and exact statement below.

theorem exists_abs_eq_maxAbsCoefficient [Nonempty (Fin s)] (a : Fin s → ℝ) : ∃ i : Fin s, |a i| = maxAbsCoefficient a

No declaration docstring is present; use the chapter context and exact statement below.

def supportCombination (basis : Fin s → V) (a : Fin s → ℝ) : V

No declaration docstring is present; use the chapter context and exact statement below.

def signedSupportAtom (coefficient : ℝ) (atom : V) : V

No declaration docstring is present; use the chapter context and exact statement below.

theorem signedSupportAtom_mem (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) (i : Fin s) : signedSupportAtom (a i) (basis i) ∈ system.atoms

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQ_supportCombination_le [Nonempty (Fin s)] (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : system.sourceQ (supportCombination basis a) ≤ maxAbsCoefficient a

No declaration docstring is present; use the chapter context and exact statement below.

theorem inner_supportCombination_basis (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) (m : Fin s) : ⟪supportCombination basis a, basis m⟫_ℝ = a m

No declaration docstring is present; use the chapter context and exact statement below.

theorem inner_supportCombination_signedSupportAtom (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) (m : Fin s) : ⟪supportCombination basis a, signedSupportAtom (a m) (basis m)⟫_ℝ = |a m|

Source Lemma 3.1: `Q` is the coefficient maximum on a succinct support.

theorem sourceQ_supportCombination_eq [Nonempty (Fin s)] (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : system.sourceQ (supportCombination basis a) = maxAbsCoefficient a

No declaration docstring is present; use the chapter context and exact statement below.

def coefficientSign (coefficient : ℝ) : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem abs_coefficientSign (coefficient : ℝ) : |coefficientSign coefficient| = 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem coefficientSign_mul (coefficient : ℝ) : coefficientSign coefficient * coefficient = |coefficient|

No declaration docstring is present; use the chapter context and exact statement below.

theorem coefficientSign_coefficientSign (coefficient : ℝ) : coefficientSign (coefficientSign coefficient) = coefficientSign coefficient

No declaration docstring is present; use the chapter context and exact statement below.

theorem coefficientSign_mul_self (coefficient : ℝ) : coefficientSign coefficient * coefficientSign coefficient = 1

No declaration docstring is present; use the chapter context and exact statement below.

def supportSignCombination (basis : Fin s → V) (a : Fin s → ℝ) : V

No declaration docstring is present; use the chapter context and exact statement below.

theorem maxAbsCoefficient_coefficientSign [Nonempty (Fin s)] (a : Fin s → ℝ) : maxAbsCoefficient (fun i => coefficientSign (a i)) = 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQ_supportSignCombination [Nonempty (Fin s)] (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : system.sourceQ (supportSignCombination basis a) = 1

The sign sum used in Appendix A.3 has squared norm equal to the support size.

theorem norm_sq_supportSignCombination [Nonempty (Fin s)] (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : ‖supportSignCombination basis a‖ ^ 2 = (s : ℝ)

No declaration docstring is present; use the chapter context and exact statement below.

theorem inner_supportCombination_supportSignCombination (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : ⟪supportCombination basis a, supportSignCombination basis a⟫_ℝ = ∑ i, |a i|

No declaration docstring is present; use the chapter context and exact statement below.

theorem inner_supportCombination_le_sumAbs_mul_sourceQ (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) (y : V) : |⟪supportCombination basis a, y⟫_ℝ| ≤ (∑ i, |a i|) * system.sourceQ y

No declaration docstring is present; use the chapter context and exact statement below.

theorem inner_supportCombination_le_sumAbs_of_sourceQ_le_one (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) {y : V} (hy : system.sourceQ y ≤ 1) : ⟪supportCombination basis a, y⟫_ℝ ≤ ∑ i, |a i|

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceRSet_bddAbove (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : BddAbove ((fun y : V => ⟪supportCombination basis a, y⟫_ℝ) '' {y | system.sourceQ y ≤ 1})

Source Lemma 3.2 for a succinct vector. The proof also supplies the boundedness evidence missing from a bare use of real `sSup`.

theorem sourceR_supportCombination_eq [Nonempty (Fin s)] (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : system.sourceR (supportCombination basis a) = ∑ i, |a i|

Source Definition 3.3, represented with its witness data exposed. The positive support-size premise is recorded explicitly.

structure SuccinctRepresentation (system : SuccinctUnitSystem V) (x : V) (s : Nat) where

The strict clause in source Definition 3.3: every coefficient in the chosen succinct representation is nonzero.

structure StrictSuccinctRepresentation (system : SuccinctUnitSystem V) (x : V) (s : Nat) extends SuccinctRepresentation system x s where

Proposition-level source wording: `x` admits an `s`-succinct representation.

def IsSuccinctAt (system : SuccinctUnitSystem V) (x : V) (s : Nat) : Prop

Proposition-level source wording: `x` admits a strictly `s`-succinct representation.

def IsStrictlySuccinctAt (system : SuccinctUnitSystem V) (x : V) (s : Nat) : Prop

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceR_eq_sumAbs (representation : SuccinctRepresentation system x s) : system.sourceR x = ∑ i, |representation.coefficients i|

No declaration docstring is present; use the chapter context and exact statement below.

theorem inner_supportSignCombination_eq_sumAbs (representation : SuccinctRepresentation system x s) : ⟪x, IsSuccinctSupport.supportSignCombination representation.basis representation.coefficients⟫_ℝ = ∑ i, |representation.coefficients i|

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceQ_supportSignCombination_eq_one (representation : SuccinctRepresentation system x s) : system.sourceQ (IsSuccinctSupport.supportSignCombination representation.basis representation.coefficients) = 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem norm_sq_supportSignCombination_eq_size (representation : SuccinctRepresentation system x s) : ‖IsSuccinctSupport.supportSignCombination representation.basis representation.coefficients‖ ^ 2 = (s : ℝ)

The two local Lemma-3.2 identities give equality of coefficient `l1` sums for any two succinct representations of the same vector.

theorem sumAbs_eq (first : SuccinctRepresentation system x s) (second : SuccinctRepresentation system x z) : (∑ i, |first.coefficients i|) = ∑ j, |second.coefficients j|

Appendix A.3 equality case: if the second representation is strict, every second-support atom has unit absolute correlation with the sign sum of the first support.

theorem abs_inner_strictBasis_supportSignCombination_eq_one (first : SuccinctRepresentation system x s) (second : StrictSuccinctRepresentation system x z) (j : Fin z) : |⟪second.toSuccinctRepresentation.basis j, IsSuccinctSupport.supportSignCombination first.basis first.coefficients⟫_ℝ| = 1

Source Lemma 3.3 on explicit witnesses: if the same vector has an `s`-succinct representation and a strictly `z`-succinct representation, then `z <= s`.

theorem strictSize_le (first : SuccinctRepresentation system x s) (second : StrictSuccinctRepresentation system x z) : z ≤ s

No declaration docstring is present; use the chapter context and exact statement below.

theorem abs_coefficient_pos (representation : StrictSuccinctRepresentation system x s) (i : Fin s) : 0 < |representation.toSuccinctRepresentation.coefficients i|

Source Lemma 3.3 in proposition-level Definition-3.3 wording.

theorem succinctSize_ge_strictSize {system : SuccinctUnitSystem V} {x : V} {s z : Nat} (hs : IsSuccinctAt system x s) (hz : IsStrictlySuccinctAt system x z) : z ≤ s

Source Lemma 3.4: two strict succinct representations of the same vector have the same size.

theorem strictlySuccinctSize_unique {system : SuccinctUnitSystem V} {x : V} {s z : Nat} (hs : IsStrictlySuccinctAt system x s) (hz : IsStrictlySuccinctAt system x z) : s = z