OAI/Probability/SKGap/Localization/ResidualMultiplier.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Static.starSquared line 14
  2. def OAI.SKGapCutoff.Static.starNorm line 17
  3. lemma OAI.SKGapCutoff.Static.starSquared_nonneg line 19
  4. lemma OAI.SKGapCutoff.Static.halfDiff_mul_flipped line 23
  5. lemma OAI.SKGapCutoff.Static.multiplier_energy line 30
  6. lemma OAI.SKGapCutoff.Static.multiplier_starSquared line 69
  7. lemma OAI.SKGapCutoff.Static.star_multiplier line 87
  8. lemma OAI.SKGapCutoff.Static.expected_abs_le_star line 95
  9. lemma OAI.SKGapCutoff.Static.sqrt_energy_le_star line 104
  10. theorem OAI.SKGapCutoff.Static.signed_base_star line 109
  11. def OAI.SKGapCutoff.Static.UniformMultiplier line 132
  12. def OAI.SKGapCutoff.Static.UniformWeak line 136
  13. lemma OAI.SKGapCutoff.Static.UniformWeak.zero line 139
  14. lemma OAI.SKGapCutoff.Static.UniformWeak.congr line 143
  15. lemma OAI.SKGapCutoff.Static.UniformWeak.add line 148
  16. lemma OAI.SKGapCutoff.Static.UniformWeak.neg line 156
  17. lemma OAI.SKGapCutoff.Static.UniformWeak.sub line 162
  18. lemma OAI.SKGapCutoff.Static.UniformWeak.sum line 166
  19. lemma OAI.SKGapCutoff.Static.UniformWeak.mul line 177
  20. lemma OAI.SKGapCutoff.Static.UniformMultiplier.const line 191
  21. lemma OAI.SKGapCutoff.Static.UniformWeak.smul line 196
  22. lemma OAI.SKGapCutoff.Static.UniformWeak.base line 200
  23. lemma OAI.SKGapCutoff.Static.UniformMultiplier.normedMean line 211