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

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Finite interval cells of appendix §07. Actual tagged values.

  1. inductive OAI.GeneralMahler.SCal.Tag line 10
  2. instance OAI.GeneralMahler.SCal.Tag.(instance at line 15) line 15
  3. def OAI.GeneralMahler.SCal.Tag.Fld line 19
  4. def OAI.GeneralMahler.SCal.Tag.act line 37
  5. def OAI.GeneralMahler.SCal.Tag.Jt line 56
  6. lemma OAI.GeneralMahler.SCal.Tag.tower line 74
  7. lemma OAI.GeneralMahler.SCal.Tag.FldK line 93
  8. lemma OAI.GeneralMahler.SCal.Tag.FldC line 94
  9. lemma OAI.GeneralMahler.SCal.Tag.field_val line 95
  10. lemma OAI.GeneralMahler.SCal.Tag.fit line 118
  11. def OAI.GeneralMahler.SCal.Grid.nd line 142

    Source comment

    finite mesh: t_j=j/200
    noncomputable def nd (n:ℕ):ℝ:= n/200
  12. def OAI.GeneralMahler.SCal.Grid.deltG line 143
  13. def OAI.GeneralMahler.SCal.Grid.nbox line 144
  14. lemma OAI.GeneralMahler.SCal.Grid.mgrid line 145
  15. lemma OAI.GeneralMahler.SCal.Grid.n_nn line 146
  16. lemma OAI.GeneralMahler.SCal.Grid.dcell line 147
  17. def OAI.GeneralMahler.SCal.Grid.pG line 151
  18. def OAI.GeneralMahler.SCal.Grid.pc line 152
  19. lemma OAI.GeneralMahler.SCal.Grid.pGa line 153
  20. lemma OAI.GeneralMahler.SCal.Grid.pca line 154
  21. def OAI.GeneralMahler.SCal.Grid.cb0 line 157
  22. def OAI.GeneralMahler.SCal.Grid.cb line 159
  23. def OAI.GeneralMahler.SCal.Grid.sharp line 160
  24. def OAI.GeneralMahler.SCal.Grid.tot line 163
  25. lemma OAI.GeneralMahler.SCal.Grid.hcb0 line 164
  26. lemma OAI.GeneralMahler.SCal.Grid.hcb line 171
  27. lemma OAI.GeneralMahler.SCal.Grid.htot line 176