OAI/Analysis/BiholderTransport/Oscillation/SectionOscillation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakMTWTransport.sectionOscillation line 21
  2. lemma OAI.WeakMTWTransport.isCompact_gapSection line 25
  3. lemma OAI.WeakMTWTransport.gapSection_nonempty line 30
  4. lemma OAI.WeakMTWTransport.sectionOscillation_extrema line 36
  5. lemma OAI.WeakMTWTransport.sectionOscillation_nonneg line 57
  6. lemma OAI.WeakMTWTransport.sectionOscillation_mono line 64
  7. lemma OAI.WeakMTWTransport.sectionOscillation_le_diam_sq line 75
  8. def OAI.WeakMTWTransport.densityDualClass line 95
  9. lemma OAI.WeakMTWTransport.densityDualClass_nonempty line 104
  10. lemma OAI.WeakMTWTransport.densityDualClass_isDual line 117
  11. def OAI.WeakMTWTransport.classSectionOscillations line 124
  12. def OAI.WeakMTWTransport.classOscillation line 128
  13. lemma OAI.WeakMTWTransport.classSectionOscillations_nonempty line 132
  14. lemma OAI.WeakMTWTransport.classSectionOscillations_bddAbove line 139
  15. lemma OAI.WeakMTWTransport.sectionOscillation_le_classOscillation line 147
  16. lemma OAI.WeakMTWTransport.classOscillation_bounds line 154
  17. lemma OAI.WeakMTWTransport.classOscillation_monotone line 168
  18. lemma OAI.WeakMTWTransport.exists_section_with_large_oscillation line 179
  19. def OAI.WeakMTWTransport.reverseNormalizedPair line 194
  20. lemma OAI.WeakMTWTransport.reverseNormalizedPair_mem line 200
  21. lemma OAI.WeakMTWTransport.densityDualClass_reverse line 224
  22. lemma OAI.WeakMTWTransport.reverseNormalizedPair_gap line 245
  23. lemma OAI.WeakMTWTransport.exists_small_step line 256
  24. lemma OAI.WeakMTWTransport.logarithmic_plateau_quantitative line 268
  25. def OAI.WeakMTWTransport.HasPowerUpperBound line 323
  26. lemma OAI.WeakMTWTransport.log_sublinear_of_no_power line 327
  27. lemma OAI.WeakMTWTransport.logarithmic_profile_nonneg line 346
  28. lemma OAI.WeakMTWTransport.logarithmic_profile_monotone line 353
  29. lemma OAI.WeakMTWTransport.no_power_logarithmic_plateau line 361
  30. lemma OAI.WeakMTWTransport.positive_of_no_power line 373
  31. lemma OAI.WeakMTWTransport.no_power_gap_scale_plateau line 382