OAI/Geometry/Convex/GeneralMahler/Linear/Powers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Eq25 scalar-functional profiles.

  1. lemma OAI.GeneralMahler.Profile.testC line 13
  2. lemma OAI.GeneralMahler.Profile.testK line 15
  3. lemma OAI.GeneralMahler.Profile.KN line 17
  4. lemma OAI.GeneralMahler.Profile.Kzero line 20
  5. lemma OAI.GeneralMahler.Profile.Dadd line 26
  6. lemma OAI.GeneralMahler.Profile.Dmul line 29
  7. lemma OAI.GeneralMahler.Profile.N2sum line 32
  8. lemma OAI.GeneralMahler.Profile.N2scale line 35
  9. lemma OAI.GeneralMahler.Profile.ND line 39
  10. lemma OAI.GeneralMahler.Profile.ND2 line 44
  11. lemma OAI.GeneralMahler.Profile.second_f line 52
  12. lemma OAI.GeneralMahler.Profile.second_D line 56
  13. lemma OAI.GeneralMahler.Profile.second_C line 61
  14. lemma OAI.GeneralMahler.Profile.exists_N line 74

    Source comment

    use any second primitive; tilt so first derivatives match
    lemma exists_N (hf:TestF f) (hh:TestF h)
    (he:deriv (deriv f)=N2 h) :
    ∃ F:ℝ→ℝ, TestF F ∧ deriv (deriv F)=h ∧ deriv f=deriv (N F) := by
…

    Mentions: OAI.GeneralMahler.TestF, OAI.GeneralMahler.Profile.f, OAI.GeneralMahler.Profile.N2, OAI.GeneralMahler.Profile.N

  15. lemma OAI.GeneralMahler.ProjField.rm_diff line 103
  16. lemma OAI.GeneralMahler.ProjField.DelP_form line 107