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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Pointwise scalar covariance and layer inequalities.

  1. lemma OAI.GeneralMahler.SCal.SQrange line 10
  2. lemma OAI.GeneralMahler.SCal.Qrange line 16
  3. lemma OAI.GeneralMahler.SCal.onPanels line 23

    Source comment

    choose one rectangle for each parameter
    lemma onPanels (h:NG) (t:ℝ) :
    ∃ k:ℕ,k≤8 ∧ SIn (fun i=>i.act t) (panel k) ∧
      ro2 t≤ rPanel k^2 := by
…

    Mentions: OAI.GeneralMahler.SCal.NG, OAI.GeneralMahler.SCal.ro2, OAI.GeneralMahler.SCal.rPanel

  4. lemma OAI.GeneralMahler.SCal.Sp_upper line 38
  5. lemma OAI.GeneralMahler.SCal.CSr line 44
  6. lemma OAI.GeneralMahler.SCal.kk_bd line 50
  7. lemma OAI.GeneralMahler.SCal.h_contact line 52
  8. lemma OAI.GeneralMahler.SCal.PA.kstats line 65
  9. lemma OAI.GeneralMahler.SCal.PA.hMono line 70
  10. lemma OAI.GeneralMahler.SCal.layer_line line 80
  11. theorem OAI.GeneralMahler.SCal.hSeg01 line 126
  12. theorem OAI.GeneralMahler.SCal.upd_ok line 140