NTK-style Gram matrix concentration usage example

This application specializes the generic feature-Gram operator to finite-width NTK/random-feature Gram summands. It retains vector-level measurability, coordinate MemLp 2, squared-vector-norm radii, and vector-level independence; the caller never states independence of centered matrix summands.

@[reducible, inline]

abbrev HighDimProb.Examples.RandomMatrix.NTKGramUsage.NTKFeatureVector (n : ℕ) : Type

@[reducible, inline]

abbrev HighDimProb.Examples.RandomMatrix.NTKGramUsage.RandomNTKFeatureVector (Omega : Type u_1) [MeasurableSpace Omega] (n : ℕ) : Type u_1

def HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramOuter {n : ℕ} (v : NTKFeatureVector n) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

@[simp]

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramOuter_apply {n : ℕ} (v : NTKFeatureVector n) (i j : Fin (n + 1)) : ntkGramOuter v i j = v i * v j

def HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramContribution {Omega : Type u_1} [MeasurableSpace Omega] {n : ℕ} (J : RandomNTKFeatureVector Omega n) : RandomMatrix Omega (n + 1) (n + 1)

@[simp]

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramContribution_apply {Omega : Type u_1} [MeasurableSpace Omega] {n : ℕ} (J : RandomNTKFeatureVector Omega n) (omega : Omega) (i j : Fin (n + 1)) : ntkGramContribution J omega i j = J omega i * J omega j

@[reducible, inline]

noncomputable abbrev HighDimProb.Examples.RandomMatrix.NTKGramUsage.centeredNTKGramContribution {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n : ℕ} (J : RandomNTKFeatureVector Omega n) : RandomMatrix Omega (n + 1) (n + 1)

@[reducible, inline]

noncomputable abbrev HighDimProb.Examples.RandomMatrix.NTKGramUsage.centeredNTKGramSummands {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) : Fin width → RandomMatrix Omega (n + 1) (n + 1)

@[reducible, inline]

abbrev HighDimProb.Examples.RandomMatrix.NTKGramUsage.NTKGramInputs {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) (R : ℝ) (Rvar : Fin width → ℝ) : Prop

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.NTKGramInputs.ofIIndepFun {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n width : ℕ} {J : Fin width → RandomNTKFeatureVector Omega n} {R : ℝ} {Rvar : Fin width → ℝ} (randomVector : ∀ (b : Fin width), IsRandomVector P (J b)) (coordinateMemLpTwo : ∀ (b : Fin width) (j : Fin (n + 1)), MemLpRealRandomVariable P (coord (J b) j) 2) (sqNormBound : ∀ (b : Fin width) (omega : Omega), vectorSqNorm (J b omega) ≤ R) (hIndep : ProbabilityTheory.iIndepFun J P) (radiusNonneg : 0 ≤ R) (varianceSqNormBound : ∀ (b : Fin width) (omega : Omega), vectorSqNorm (J b omega) ≤ Rvar b) (varianceRadiiNonneg : ∀ (b : Fin width), 0 ≤ Rvar b) : NTKGramInputs J R Rvar

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGram_operatorNormTail {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n width : ℕ} [StandardBorelSpace (Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ)] (J : Fin width → RandomNTKFeatureVector Omega n) (R t : ℝ) (Rvar : Fin width → ℝ) (h : NTKGramInputs J R Rvar) (ht : 0 ≤ t) : upperTailProb P (operatorNorm (randomMatrixSum (centeredNTKGramSummands J))) t ≤ matrixBernsteinTwoSidedOptimizedScalarTailRHS (n + 1) (2 * R) (2 * R) t (rowSqNormVarianceProxyNormRHS Rvar) (rowSqNormVarianceProxyNormRHS Rvar)

noncomputable def HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkEmpiricalGram {Omega : Type u_1} [MeasurableSpace Omega] {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) : RandomMatrix Omega (n + 1) (n + 1)

noncomputable def HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkPopulationGram {Omega : Type u_1} [MeasurableSpace Omega] (P : MeasureTheory.Measure Omega) {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

noncomputable def HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramDeviation {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) : RandomMatrix Omega (n + 1) (n + 1)

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkEmpiricalGram_sub_population {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) (omega : Omega) : ntkEmpiricalGram J omega - ntkPopulationGram P J = ntkGramDeviation J omega

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramDeviation_upperTailProb {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) (epsilon : ℝ) (hwidth : 0 < width) : upperTailProb P (operatorNorm (ntkGramDeviation J)) epsilon = upperTailProb P (operatorNorm (randomMatrixSum (centeredNTKGramSummands J))) (↑width * epsilon)

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGram_normalizedTail {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n width : ℕ} [StandardBorelSpace (Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ)] (J : Fin width → RandomNTKFeatureVector Omega n) (R epsilon : ℝ) (Rvar : Fin width → ℝ) (h : NTKGramInputs J R Rvar) (hwidth : 0 < width) (hepsilon : 0 ≤ epsilon) : upperTailProb P (operatorNorm (ntkGramDeviation J)) epsilon ≤ matrixBernsteinTwoSidedOptimizedScalarTailRHS (n + 1) (2 * R) (2 * R) (↑width * epsilon) (rowSqNormVarianceProxyNormRHS Rvar) (rowSqNormVarianceProxyNormRHS Rvar)

noncomputable def HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramRadius (width n : ℕ) (Rvar : Fin width → ℝ) (R delta : ℝ) : ℝ

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGram_highProbability {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n width : ℕ} [StandardBorelSpace (Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ)] (J : Fin width → RandomNTKFeatureVector Omega n) (R delta : ℝ) (Rvar : Fin width → ℝ) (h : NTKGramInputs J R Rvar) (hwidth : 0 < width) (hNondegenerate : 0 < rowSqNormVarianceProxyNormRHS Rvar ∨ 0 < 2 * R) (hdelta : 0 < delta) (hdeltaOne : delta ≤ 1) : upperTailProb P (operatorNorm (ntkGramDeviation J)) (ntkGramRadius width n Rvar R delta) ≤ ENNReal.ofReal delta

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGramDeviation_selfAdjoint {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) (R : ℝ) (Rvar : Fin width → ℝ) (h : NTKGramInputs J R Rvar) (omega : Omega) : IsSelfAdjointMatrix (ntkGramDeviation J omega)

theorem HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGram_matrixLESandwich {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n width : ℕ} (J : Fin width → RandomNTKFeatureVector Omega n) (R epsilon : ℝ) (Rvar : Fin width → ℝ) (h : NTKGramInputs J R Rvar) (omega : Omega) (hNorm : deterministicOperatorNorm (ntkGramDeviation J omega) ≤ epsilon) : MatrixLE (ntkPopulationGram P J - epsilon • 1) (ntkEmpiricalGram J omega) ∧ MatrixLE (ntkEmpiricalGram J omega) (ntkPopulationGram P J + epsilon • 1)