Lean module · Foundations
BanditRLProof.CurvatureNoiseGapGeometry
# Curvature--Noise--Gap geometry: finite algebraic leaves This file contains only route-independent finite-dimensional algebra. It does not formalize the full Curvature--Noise--Gap calculus, Tsallis-INF, or a new bandit theorem. The intended later use is to test whether these abstractions replace repeated route-specific proof subgraphs and transfer to held-out proof families. The assumptions are deliberately explicit. Tangent invariance needs only a zero-sum direction. The weighted shift minimum needs nonnegative weights and strictly positive total weight; it does not hide an interiority or positive-definiteness premise.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CurvatureNoiseGap.IsSimplexTangent
Compiled
A finite direction tangent to the affine simplex hyperplane.
def IsSimplexTangent {Index : Type*} [DecidableEq Index] (indices : Finset Index) (direction : Index -> Real) : Prop
def
BanditRLProof.CurvatureNoiseGap.tangentPairing
Compiled
The finite pairing used to test a signal against a tangent direction.
def tangentPairing {Index : Type*} [DecidableEq Index] (indices : Finset Index) (signal direction : Index -> Real) : Real
theorem
BanditRLProof.CurvatureNoiseGap.tangentPairing_add_const_of_isSimplexTangent
Compiled
Adding a constant to a signal is invisible on the simplex tangent space.
theorem tangentPairing_add_const_of_isSimplexTangent {Index : Type*} [DecidableEq Index] (indices : Finset Index) (signal direction : Index -> Real) (shift : Real) (hdirection : IsSimplexTangent indices direction) : tangentPairing indices (fun i => signal i + shift) direction = tangentPairing indices signal direction
def
BanditRLProof.CurvatureNoiseGap.weightedShiftEnergy
Compiled
Weighted squared energy after removing one common scalar shift.
def weightedShiftEnergy {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal : Index -> Real) (shift : Real) : Real
def
BanditRLProof.CurvatureNoiseGap.weightedCenter
Compiled
The scalar shift selected by a nondegenerate weighted quadratic energy.
noncomputable def weightedCenter {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal : Index -> Real) : Real
theorem
BanditRLProof.CurvatureNoiseGap.sum_weight_mul_sub_weightedCenter_eq_zero
Compiled
The weighted residual about `weightedCenter` has zero weighted sum.
theorem sum_weight_mul_sub_weightedCenter_eq_zero {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal : Index -> Real) (hweightSum : indices.sum weight ≠ 0) : indices.sum (fun i => weight i * (signal i - weightedCenter indices weight signal)) = 0
theorem
BanditRLProof.CurvatureNoiseGap.weightedShiftEnergy_decomposition_of_centered
Compiled
Completing the square around any weighted-centered scalar.
theorem weightedShiftEnergy_decomposition_of_centered {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal : Index -> Real) (center shift : Real) (hcenter : indices.sum (fun i => weight i * (signal i - center)) = 0) : weightedShiftEnergy indices weight signal shift = weightedShiftEnergy indices weight signal center + indices.sum weight * (shift - center) ^ 2
theorem
BanditRLProof.CurvatureNoiseGap.weightedShiftEnergy_decomposition
Compiled
Exact min-shift decomposition at the weighted center.
theorem weightedShiftEnergy_decomposition {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal : Index -> Real) (shift : Real) (hweightSum : indices.sum weight ≠ 0) : weightedShiftEnergy indices weight signal shift = weightedShiftEnergy indices weight signal (weightedCenter indices weight signal) + indices.sum weight * (shift - weightedCenter indices weight signal) ^ 2
theorem
BanditRLProof.CurvatureNoiseGap.weightedShiftEnergy_center_le
Compiled
The weighted center minimizes the quadratic shift energy.
theorem weightedShiftEnergy_center_le {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal : Index -> Real) (shift : Real) (hweight : forall i, i ∈ indices -> 0 <= weight i) (hweightSum : 0 < indices.sum weight) : weightedShiftEnergy indices weight signal (weightedCenter indices weight signal) <= weightedShiftEnergy indices weight signal shift
theorem
BanditRLProof.CurvatureNoiseGap.weightedShiftEnergy_eq_center_iff
Compiled
Strict positivity of the total weight makes the minimizing shift unique.
theorem weightedShiftEnergy_eq_center_iff {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal : Index -> Real) (shift : Real) (hweightSum : 0 < indices.sum weight) : weightedShiftEnergy indices weight signal shift = weightedShiftEnergy indices weight signal (weightedCenter indices weight signal) <-> shift = weightedCenter indices weight signal
theorem
BanditRLProof.CurvatureNoiseGap.weightedShiftEnergy_add_decomposition
Compiled
Exact signal--noise decomposition, including the interaction term.
theorem weightedShiftEnergy_add_decomposition {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal noise : Index -> Real) (signalShift noiseShift : Real) : weightedShiftEnergy indices weight (fun i => signal i + noise i) (signalShift + noiseShift) = weightedShiftEnergy indices weight signal signalShift + weightedShiftEnergy indices weight noise noiseShift + 2 * indices.sum (fun i => weight i * (signal i - signalShift) * (noise i - noiseShift))
theorem
BanditRLProof.CurvatureNoiseGap.weightedShiftEnergy_add_le_two
Compiled
A conservative two-term signal--noise energy bound.
theorem weightedShiftEnergy_add_le_two {Index : Type*} [DecidableEq Index] (indices : Finset Index) (weight signal noise : Index -> Real) (signalShift noiseShift : Real) (hweight : forall i, i ∈ indices -> 0 <= weight i) : weightedShiftEnergy indices weight (fun i => signal i + noise i) (signalShift + noiseShift) <= 2 * weightedShiftEnergy indices weight signal signalShift + 2 * weightedShiftEnergy indices weight noise noiseShift