OAI/Geometry/Convex/GeneralMahler/Scalar/LayerAlg.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

§07 layer rectangles. Evaluate only 4 vertices in H and V2.

  1. def OAI.GeneralMahler.SCal.PA.endp line 8
  2. def OAI.GeneralMahler.SCal.PA.eR line 11
  3. def OAI.GeneralMahler.SCal.PA.eB line 12
  4. lemma OAI.GeneralMahler.SCal.PA.ek line 13
  5. lemma OAI.GeneralMahler.SCal.PA.orderE line 14
  6. def OAI.GeneralMahler.SCal.PA.Ldef line 17
  7. def OAI.GeneralMahler.SCal.PA.Lcost line 20
  8. def OAI.GeneralMahler.SCal.PA.HV line 22
  9. def OAI.GeneralMahler.SCal.PA.defB line 23
  10. def OAI.GeneralMahler.SCal.PA.bmb line 26
  11. def OAI.GeneralMahler.SCal.PA.fixedCost line 30

    Source comment

    The fixed term in the layer inequality.
    noncomputable def fixedCost := 2*(bb+eta+(bb+eta-kar)*tmin)+ 2*e₀*(2*Profile.tr)^2+Profile.tr*h₀/2

    Mentions: OAI.GeneralMahler.tmin, OAI.GeneralMahler.Profile.tr

  12. lemma OAI.GeneralMahler.SCal.PA.mnums line 32

    Source comment

    Rational interval enclosures for the layer constants.
    lemma mnums :
    Profile.tc∈bd 210∧ kar∈bd 11600 ∧ Profile.tr∈bd 430 ∧ h₀ ∈ bd 5000 ∧
      alpha∈ bd 22600 ∧ tmin∈bd (-220) ∧ eta∈bd 220 ∧ e₀∈bd 2560 := by
…

    Mentions: OAI.GeneralMahler.Profile.tc, OAI.GeneralMahler.Profile.tr, OAI.GeneralMahler.tmin

  13. lemma OAI.GeneralMahler.SCal.PA.mDef line 39
  14. lemma OAI.GeneralMahler.SCal.PA.mBBc line 44
  15. lemma OAI.GeneralMahler.SCal.PA.mthree line 48
  16. lemma OAI.GeneralMahler.SCal.PA.mfour line 49
  17. lemma OAI.GeneralMahler.SCal.PA.mbMc line 50
  18. def OAI.GeneralMahler.SCal.PA.costB line 55
  19. lemma OAI.GeneralMahler.SCal.PA.mCost line 58
  20. def OAI.GeneralMahler.SCal.PA.hvB line 64
  21. lemma OAI.GeneralMahler.SCal.PA.mHV line 65
  22. def OAI.GeneralMahler.SCal.PA.Hbnd line 68
  23. def OAI.GeneralMahler.SCal.PA.hbB line 70
  24. lemma OAI.GeneralMahler.SCal.PA.hBm line 73
  25. def OAI.GeneralMahler.SCal.PA.cond line 81
  26. def OAI.GeneralMahler.SCal.PA.corners line 84
  27. def OAI.GeneralMahler.SCal.PA.allCn line 86
  28. lemma OAI.GeneralMahler.SCal.PA.passC line 87
  29. lemma OAI.GeneralMahler.SCal.PA.corner_pos line 89
  30. lemma OAI.GeneralMahler.SCal.PA.lpos line 101
  31. lemma OAI.GeneralMahler.SCal.PA.whole line 117