OAI/Geometry/Convex/GeneralMahler/CDF.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

One-dimensional Gaussian layers, preliminary identities and bounds (§§01--02).

  1. def OAI.GeneralMahler.Layers.p line 11
  2. def OAI.GeneralMahler.Layers.a line 12
  3. lemma OAI.GeneralMahler.Layers.d_phi line 14
  4. lemma OAI.GeneralMahler.Layers.c_phi line 20
  5. lemma OAI.GeneralMahler.Layers.i_phi line 22
  6. lemma OAI.GeneralMahler.Layers.e_phi line 23
  7. lemma OAI.GeneralMahler.Layers.int_Ioi line 25
  8. lemma OAI.GeneralMahler.Layers.neg_phi line 31
  9. lemma OAI.GeneralMahler.Layers.neg_p line 33
  10. lemma OAI.GeneralMahler.Layers.p_half line 45
  11. lemma OAI.GeneralMahler.Layers.d_p line 49
  12. lemma OAI.GeneralMahler.Layers.d_a line 58
  13. lemma OAI.GeneralMahler.Layers.cp line 63
  14. lemma OAI.GeneralMahler.Layers.ca line 64
  15. lemma OAI.GeneralMahler.Layers.p_pos line 65
  16. lemma OAI.GeneralMahler.Layers.p_lt_one line 72
  17. lemma OAI.GeneralMahler.Layers.p_mono line 76
  18. lemma OAI.GeneralMahler.Layers.a_mono line 79
  19. lemma OAI.GeneralMahler.Layers.phi_bdd line 82
  20. lemma OAI.GeneralMahler.Layers.int_moment1 line 87
  21. lemma OAI.GeneralMahler.Layers.moment1 line 94
  22. lemma OAI.GeneralMahler.Layers.int_gap line 105
  23. lemma OAI.GeneralMahler.Layers.a_eq line 109
  24. lemma OAI.GeneralMahler.Layers.a_pos line 116
  25. lemma OAI.GeneralMahler.Layers.a_high line 127

    Source comment

    Two-sided estimates, exact constants unimportant here.
    lemma a_high (s : ℝ) (hs : 0 ≤ s) : a (-s) ≤ phi s := by
…

    Mentions: OAI.GeneralMahler.Layers.a, OAI.GeneralMahler.phi

  26. lemma OAI.GeneralMahler.Layers.a_low line 131