LogEndpoint.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

This is the missing metric step between Fourier smoothing in log norm and the summable endpoint kernel in the norm variable.

theorem OAI.CubicFirstMoment.sub_le_mul_log_sub line 16
theorem OAI.CubicFirstMoment.abs_sub_le_four_mul_log_distance line 24
theorem OAI.CubicFirstMoment.reciprocal_sq_le_endpoint line 38
theorem OAI.CubicFirstMoment.log_boundary_le_endpoint line 49
Source documentation
On the fixed norm envelope, the Fourier boundary majorant is at most an absolute constant times the summable integer endpoint kernel.
```
theorem log_boundary_le_endpoint {X T n b : ℝ}
    (hX : 0 < X) (hT : 0 < T) (hn : 0 < n) (hn4 : n ≤ 4*X)
    (hb : 0 < b) (hb4 : b ≤ 4) :
    1 / (1 + T*|Real.log (n/X) - Real.log b|)^2 ≤
      16 * endpointKernel (X/T) (n - b*X) := by
…
```
Mentions: OAI.CubicFirstMoment.endpointKernel