OAI/Geometry/Convex/GeneralMahler/AngleIntegral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Diagonal balance, with separate estimates at the two ends of the coordinate box.

  1. def OAI.GeneralMahler.ek line 13

    Source comment

    Polynomial coefficient D as in angle_est.
    def ek (j : ℝ) := Real.exp (-(j^2)/4)
  2. lemma OAI.GeneralMahler.ekpos line 15
  3. lemma OAI.GeneralMahler.ekrapid line 16
  4. lemma OAI.GeneralMahler.small_minus_bound line 20
  5. lemma OAI.GeneralMahler.small_plus_lower line 54
  6. lemma OAI.GeneralMahler.large_minus_lower line 78
  7. lemma OAI.GeneralMahler.large_core_upper line 104
  8. lemma OAI.GeneralMahler.plus_split line 130