OAI/Analysis/NefAdjoint/SectionGauge.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NefAdjoint.SectionGauge.first_holder line 13
  2. theorem OAI.NefAdjoint.SectionGauge.mixture_bound line 33
  3. theorem OAI.NefAdjoint.SectionGauge.two_holder_bound line 57
  4. def OAI.NefAdjoint.SectionGauge.expDensity line 69
  5. lemma OAI.NefAdjoint.SectionGauge.expDensity_add line 71
  6. lemma OAI.NefAdjoint.SectionGauge.expDensity_mul line 75
  7. lemma OAI.NefAdjoint.SectionGauge.expDensity_mono line 80
  8. lemma OAI.NefAdjoint.SectionGauge.expDensity_max line 84
  9. lemma OAI.NefAdjoint.SectionGauge.aemeasurable_expDensity line 90
  10. def OAI.NefAdjoint.SectionGauge.sourceG line 93
  11. theorem OAI.NefAdjoint.SectionGauge.canonical_density_mixture line 96
  12. theorem OAI.NefAdjoint.SectionGauge.exponential_density_mixture line 111
  13. lemma OAI.NefAdjoint.SectionGauge.real_gauge_factorization line 120
  14. lemma OAI.NefAdjoint.SectionGauge.gauge_factorization line 135
  15. theorem OAI.NefAdjoint.SectionGauge.source_gauge_bound line 146
  16. theorem OAI.NefAdjoint.SectionGauge.tail_mass_tendsto_zero line 176
  17. theorem OAI.NefAdjoint.SectionGauge.eventually_gauge_lt_one line 211
  18. theorem OAI.NefAdjoint.SectionGauge.normalize_gauge line 229
  19. theorem OAI.NefAdjoint.SectionGauge.isCompact_unit_gauge line 236
  20. theorem OAI.NefAdjoint.SectionGauge.exists_extremal line 270
  21. theorem OAI.NefAdjoint.SectionGauge.no_smaller_competitor line 293