OAI/Geometry/Convex/GeneralMahler/Cutoff.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform cutoffs for the biased projections. We strengthen the negative-tail estimate of the manuscript to an exact cutoff (in z, depending linearly on |g|); this makes mixed-integrability statements for the Jacobian fields simpler.

  1. def OAI.GeneralMahler.ProjField.cutoffC line 16
  2. theorem OAI.GeneralMahler.ProjField.positive_exact line 18
  3. theorem OAI.GeneralMahler.ProjField.positive_cutoff line 62
  4. theorem OAI.GeneralMahler.ProjField.negative_cutoff line 67