OAI/Geometry/Convex/GeneralMahler/LogPath.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Path z↦c(z)I+∫_{-∞}^z WP, for fixed standard input.

  1. def OAI.GeneralMahler.Edge.H line 14
  2. lemma OAI.GeneralMahler.Edge.H_diff line 15
  3. lemma OAI.GeneralMahler.Edge.H_nonneg line 20
  4. lemma OAI.GeneralMahler.Edge.H_lip line 22
  5. lemma OAI.GeneralMahler.Edge.H_deriv line 31
  6. def OAI.GeneralMahler.Edge.path line 39
  7. lemma OAI.GeneralMahler.Edge.path_pd line 40
  8. lemma OAI.GeneralMahler.Edge.path_d line 43
  9. lemma OAI.GeneralMahler.Edge.path_lip line 51
  10. def OAI.GeneralMahler.Edge.Fedge line 60
  11. lemma OAI.GeneralMahler.Edge.F_AC line 61
  12. def OAI.GeneralMahler.Edge.Sh line 77
  13. def OAI.GeneralMahler.Edge.beta line 78
  14. def OAI.GeneralMahler.Edge.h1 line 79
  15. lemma OAI.GeneralMahler.Edge.Sh_nonneg line 80
  16. lemma OAI.GeneralMahler.Edge.beta_bound line 82
  17. lemma OAI.GeneralMahler.Edge.Fedge_d line 88
  18. lemma OAI.GeneralMahler.Edge.path_neg line 114

    Source comment

    Endpoint saturation from cutoff
    lemma path_neg {z:ℝ} (h : z < -e.radius x) :
    e.H x z=0 ∧ e.Fedge x z=LC z ∧ e.beta x z=0 ∧ e.h1 x z=0 := by
…
  19. lemma OAI.GeneralMahler.Edge.path_pos line 128