PlanarEstimates.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

An elementary uniform reciprocal-arctangent estimate for the planar construction, with the explicit absolute constant C=2.

lemma OAI.SymmetricMahler.arctan_le_argument line 18
lemma OAI.SymmetricMahler.half_argument_le_arctan line 22
theorem OAI.SymmetricMahler.reciprocal_arctan_bound line 37
Source documentation
A uniform reciprocal bound with the explicit absolute constant 2.
```
theorem reciprocal_arctan_bound {v : ℝ} (hv : 0 < v) :
    1 / arctan v ≤ 2 / Real.pi + 2 / v := by
…
```
def OAI.SymmetricMahler.angularSpeed line 68
Source documentation
The angular-speed expression B as a real scalar function.
```
noncomputable def angularSpeed (r θ : ℝ) : ℝ :=
…
```

theorem OAI.SymmetricMahler.angular_speed_inverse_bound line 72

Source documentation

The reciprocal angular-speed estimate, with C = π²/4.

theorem angular_speed_inverse_bound {r θ : ℝ}
    (hr : 0 < r) (hr1 : r < 1) (hθ : 0 < sin θ) :
    1 / angularSpeed r θ ≤ Real.pi / 2 +
      (Real.pi^2 / 4) * ((1-r^2) / (r * sin θ)) := by
…

Mentions: OAI.SymmetricMahler.angularSpeed

theorem OAI.SymmetricMahler.tail_first_half line 92

Source documentation

The pointwise estimate on the first half of the tail integral.

theorem tail_first_half {L t : ℝ} (hL : 0 < L) (_ht : 0 ≤ t)
    (htL : t ≤ L/2) :
    exp (-t) * sqrt (t/(L-t)) ≤ exp (-t) := by
…

theorem OAI.SymmetricMahler.tail_second_half line 103

Source documentation

The pointwise integrable singular majorant on the second half.

theorem tail_second_half {L t : ℝ} (_hL : 0 < L)
    (ht : L/2 ≤ t) (htL : t < L) :
    exp (-t) * sqrt (t/(L-t)) ≤
      exp (-L/2) * sqrt L / sqrt (L-t) := by
…

theorem OAI.SymmetricMahler.uniform_tail_constant line 120
Source documentation
The elementary maximization for the uniform-L bound.
```
theorem uniform_tail_constant (L : ℝ) :
    1 + 2*L*exp (-L/2) ≤ 1 + 4/exp 1 := by
…
```