OAI/Geometry/TriangularCovering/Asymptotics.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularCovering.inv_sqrt_remainder line 12

   Source documentation

   An elementary quantitative Taylor bound, with an absolute constant.

   lemma inv_sqrt_remainder {x : ℝ} (hx : 0 ≤ x) :
       |1 / Real.sqrt (1+x) - (1-x/2)| ≤ x^2 := by
   …

2. lemma OAI.TriangularCovering.bounded_product_remainder line 36
3. lemma OAI.TriangularCovering.term_remainder line 76
4. lemma OAI.TriangularCovering.d_lipschitz line 105
5. lemma OAI.TriangularCovering.cutoffCoeff_error line 120
6. lemma OAI.TriangularCovering.sq_error line 134
7. def OAI.TriangularCovering.areaDensity line 141

   Source documentation

   The limiting polynomial for the second-order area coefficient.

   def areaDensity (q : ℝ) : ℝ :=
   …

8. lemma OAI.TriangularCovering.areaDensity_eq line 144
9. lemma OAI.TriangularCovering.continuous_areaDensity line 148
10. lemma OAI.TriangularCovering.density_error line 152
11. lemma OAI.TriangularCovering.areaDensity_integral line 184
12. lemma OAI.TriangularCovering.interval_density_error line 201
13. lemma OAI.TriangularCovering.count_step line 219
14. def OAI.TriangularCovering.coefficientSum line 224
15. lemma OAI.TriangularCovering.integral_mesh_sum line 227
16. lemma OAI.TriangularCovering.coefficientSum_error line 234
17. lemma OAI.TriangularCovering.mesh_term_remainder line 261
18. lemma OAI.TriangularCovering.uniform_scalar_sum line 302

    Source documentation

    Quantitative fourth-order error, independent of the number of intervals.

    lemma uniform_scalar_sum {ε : ℝ} {N : ℕ} (he : |ε| ≤ 1) (hN : 0 < N)
        (hstep : step N ≤ ε^2) :
        |(∑ j : Fin N, normalizedTerm ε (mesh N j) (mesh N (j+1))) -
          (1/2-(13/6000:ℝ)*ε^2)| ≤ 14*ε^4 := by
    …

    Mentions: OAI.TriangularCovering.step, OAI.TriangularCovering.normalizedTerm, OAI.TriangularCovering.mesh