OAI/Analysis/Mahler/SineBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.angular_speed_upper line 9

   Source documentation

   The pointwise quadratic angular estimate.

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

   Mentions: OAI.SymmetricMahler.angularSpeed

2. lemma OAI.SymmetricMahler.angular_speed_integrable line 22
3. theorem OAI.SymmetricMahler.angular_speed_integral_bound line 29

   Source documentation

   Integrating angular speed on an arc of length d gives a d² bound.

   theorem angular_speed_integral_bound {r d : ℝ} (hr : 0 < r) (hr1 : r < 1)
       (hd : 0 ≤ d) (hdπ : d ≤ Real.pi) :
       (∫ θ in (0 : ℝ)..d, angularSpeed r θ) ≤ 4*r*d^2/(Real.pi^2*(1-r^2)) := by
   …

   Mentions: OAI.SymmetricMahler.angularSpeed

4. theorem OAI.SymmetricMahler.sine_bound_of_increment line 43

   Source documentation

   The square-root sine lower bound, with the explicit constant c=1.

   theorem sine_bound_of_increment {r d Δ : ℝ} (hr : 0 < r) (hr1 : r < 1)
       (hd : 0 ≤ d) (hdπ : d ≤ Real.pi/2)
       (hΔ : Δ ≤ 4*r*d^2/(Real.pi^2*(1-r^2))) :
       sqrt ((1-r^2)*Δ/r) ≤ sin d := by
   …

5. theorem OAI.SymmetricMahler.sine_bound_of_angular_integral line 61

   Source documentation

   The sine estimate follows directly from the angular integral identity.

   theorem sine_bound_of_angular_integral {r d Δ : ℝ} (hr : 0 < r) (hr1 : r < 1)
       (hd : 0 ≤ d) (hdπ : d ≤ Real.pi/2)
       (hΔ : Δ = ∫ θ in (0 : ℝ)..d, angularSpeed r θ) :
       sqrt ((1-r^2)*Δ/r) ≤ sin d := by
   …

   Mentions: OAI.SymmetricMahler.angularSpeed