OAI/Analysis/PureInfiniteness/SpectralRowEstimate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The sampled row error has a bound independent of the number of cells. The coefficient diagonal contributes only its uniform norm bound.

  1. lemma OAI.WeakPureInfiniteness.real_sample_square line 19
  2. lemma OAI.WeakPureInfiniteness.sampled_error_square line 35
  3. def OAI.WeakPureInfiniteness.sampledErrorRow line 51
  4. lemma OAI.WeakPureInfiniteness.sampledErrorRow_gram line 54
  5. lemma OAI.WeakPureInfiniteness.sampledErrorRow_norm_sq line 66
  6. lemma OAI.WeakPureInfiniteness.sampledErrorRow_coeff_norm_le line 74