OAI/Probability/SKGap/Localization/WeakResidual.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Static.conditionalVariance line 14
  2. def OAI.SKGapCutoff.Static.varianceEnergy line 17
  3. lemma OAI.SKGapCutoff.Static.conditionalVariance_nonneg line 20
  4. lemma OAI.SKGapCutoff.Static.conditionalVariance_le_one line 26
  5. lemma OAI.SKGapCutoff.Static.varianceEnergy_nonneg line 29
  6. lemma OAI.SKGapCutoff.Static.residual_product_identity line 34
  7. lemma OAI.SKGapCutoff.Static.diagonal_reflected_bound line 53
  8. lemma OAI.SKGapCutoff.Static.weighted_residual_derivative_bound line 75
  9. lemma OAI.SKGapCutoff.Static.energy_pair_bound line 97
  10. theorem OAI.SKGapCutoff.Static.signed_weak_residual_base line 119
  11. lemma OAI.SKGapCutoff.Static.coordinate_abs_le_of_square_sum line 130
  12. lemma OAI.SKGapCutoff.Static.energy_cross_square_bound line 137
  13. lemma OAI.SKGapCutoff.Static.energy_square_coefficient_bound line 172
  14. lemma OAI.SKGapCutoff.Static.halfDiff_square line 196
  15. theorem OAI.SKGapCutoff.Static.square_weak_residual_base line 200
  16. lemma OAI.SKGapCutoff.Static.varianceEnergy_gibbs line 238
  17. lemma OAI.SKGapCutoff.Static.sum_abs_mul_le_of_squares line 244
  18. lemma OAI.SKGapCutoff.Static.multiplier_vector_bounds line 254
  19. theorem OAI.SKGapCutoff.Static.square_multiplier_weak_residual_base line 284