OAI/Probability/SKGap/Localization/LocalUniformWeak.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Static.LocalUniformMultiplier line 15
  2. def OAI.SKGapCutoff.Static.LocalUniformWeak line 19
  3. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.zero line 22
  4. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.congr line 28
  5. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.add line 33
  6. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.neg line 41
  7. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.sub line 47
  8. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.sum line 51
  9. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.mul line 62
  10. lemma OAI.SKGapCutoff.Static.LocalUniformMultiplier.const line 76
  11. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.smul line 81
  12. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.base line 85
  13. lemma OAI.SKGapCutoff.Static.UniformWeak.localize line 96
  14. lemma OAI.SKGapCutoff.Static.UniformMultiplier.localize line 101
  15. lemma OAI.SKGapCutoff.Static.LocalUniformWeak.congr_on line 120
  16. lemma OAI.SKGapCutoff.Static.LocalUniformMultiplier.normedMean line 131
  17. lemma OAI.SKGapCutoff.Static.local_uniform_normalized_pair line 137