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

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Propagate and combine the finite/infinite and reflected ranges.

  1. def OAI.GeneralMahler.SCal.NG line 10
  2. lemma OAI.GeneralMahler.SCal.NG.good line 13
  3. lemma OAI.GeneralMahler.SCal.nd0 line 15
  4. lemma OAI.GeneralMahler.SCal.nd_m line 16
  5. lemma OAI.GeneralMahler.SCal.find_cell line 17
  6. lemma OAI.GeneralMahler.SCal.x720 line 30
  7. lemma OAI.GeneralMahler.SCal.x225 line 33
  8. lemma OAI.GeneralMahler.SCal.x280 line 36
  9. lemma OAI.GeneralMahler.SCal.find_tail line 40
  10. lemma OAI.GeneralMahler.SCal.rp_th line 45
  11. lemma OAI.GeneralMahler.SCal.rp_bound line 51
  12. lemma OAI.GeneralMahler.SCal.hrq line 62
  13. lemma OAI.GeneralMahler.SCal.hqt line 63
  14. lemma OAI.GeneralMahler.SCal.stage_size line 65
  15. lemma OAI.GeneralMahler.SCal.Propagate line 69

    Source comment

    whenever past lower index r. returns cell n and panel contains x
    lemma Propagate (h:NG) {x:ℝ} {r:ℕ} (hr:r<720) (hu:nd r ≤ x) :
    ∃ n:ℕ,r ≤ n∧ n<720∧
      nd (panel (stage n)).lo ≤ x∧ ((panel (stage n)).hi<720 → x ≤ nd (panel (stage n)).hi) ∧
      passR n (fun t=>t.act x) := by
…

    Mentions: OAI.GeneralMahler.SCal.NG

  16. lemma OAI.GeneralMahler.SCal.Sym_b line 85

    Source comment

    per-real argument assertion
    lemma Sym_b (i:Tag)(h:i.odd=true): SubB (-(rng i)) (rng i) &&
    SubB (-(roff i)) (roff i) := by cases i <;> first| decide|simp [Tag.odd] at h

    Mentions: OAI.GeneralMahler.SCal.Tag, OAI.GeneralMahler.SCal.Tag.odd

  17. lemma OAI.GeneralMahler.SCal.mRange line 87
  18. lemma OAI.GeneralMahler.SCal.mOff line 99
  19. lemma OAI.GeneralMahler.SCal.mFive line 111
  20. lemma OAI.GeneralMahler.SCal.GlobalCorr line 123