PrimitiveBound.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.sine_reciprocal_bound line 10

Source documentation

Dividing the sine lower bound yields the exact residual reciprocal estimate.

theorem sine_reciprocal_bound {r θ Δ : ℝ} (hr : 0 < r) (hr1 : r < 1)
    (hΔ : 0 < Δ) (hsine : sqrt ((1-r^2)*Δ/r) ≤ sin θ) :
    (1-r^2)/(r*sin θ) ≤ sqrt (1-r^2)/(sqrt r*sqrt Δ) := by
…

theorem OAI.SymmetricMahler.radial_primitive_density_bound line 29

Source documentation

The reciprocal angular-speed estimate converts to the error-integral density, with the explicit coefficient π.

theorem radial_primitive_density_bound {r θ Δ m : ℝ}
    (hr : 0 < r) (hr1 : r < 1) (hm : 0 ≤ m) (hΔ : 0 < Δ)
    (hsine : sqrt ((1-r^2)*Δ/r) ≤ sin θ) :
    (4*m/Real.pi)*(r^(2*m-1 : ℝ)/angularSpeed r θ) ≤
      2*m*r^(2*m-1 : ℝ) +
      Real.pi*(m*r^(2*m-3/2 : ℝ)*sqrt (1-r^2)/sqrt Δ) := by
…

Mentions: OAI.SymmetricMahler.angularSpeed

def OAI.SymmetricMahler.radialPrimitiveDensity line 60
Source documentation
The radial form of the vertical primitive, before proving its equality with the integral in the image domain.
```
noncomputable def radialPrimitiveDensity (θ : ℝ → ℝ) (m r : ℝ) : ℝ :=
…
```
lemma OAI.SymmetricMahler.radial_error_integrable line 63

theorem OAI.SymmetricMahler.radial_primitive_integrable line 70

Source documentation

The density is integrable through the potentially singular initial radius; the square-root sine bound, rather than an assumed endpoint regularity, controls it.

theorem radial_primitive_integrable {θ : ℝ → ℝ} {m r₀ s : ℝ}
    (hθ : Measurable θ) (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀) (hr₀s : r₀ ≤ s) (hs1 : s < 1)
    (hsine : ∀ r ∈ Ioo r₀ 1,
      sqrt ((1-r^2)*(radialMap r-radialMap r₀)/r) ≤ sin (θ r)) :
    IntervalIntegrable (radialPrimitiveDensity θ m) volume r₀ s := by
…

Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitiveDensity

theorem OAI.SymmetricMahler.integral_radial_leading line 107
Source documentation
The leading term of the radial primitive integrates with coefficient exactly one.
```
theorem integral_radial_leading {m a b : ℝ} (hm : 0 < m) :
    (∫ r in a..b, 2*m*r^(2*m-1 : ℝ)) = b^(2*m : ℝ)-a^(2*m : ℝ) := by
…
```

theorem OAI.SymmetricMahler.radial_primitive_integral_bound line 117

Source documentation

The radial primitive is bounded by s^(2m) plus π times the uniformly controlled error. This bound does not assert equality with the image-domain primitive.

theorem radial_primitive_integral_bound {θ : ℝ → ℝ} {m r₀ s : ℝ}
    (hθ : Measurable θ) (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀) (hr₀s : r₀ ≤ s) (hs1 : s < 1)
    (hsine : ∀ r ∈ Ioo r₀ 1,
      sqrt ((1-r^2)*(radialMap r-radialMap r₀)/r) ≤ sin (θ r)) :
    (∫ r in r₀..s, radialPrimitiveDensity θ m r) ≤
      s^(2*m : ℝ) + Real.pi*(∫ r in r₀..(1 : ℝ), errorIntegrand radialMap r₀ m r) := by
…

Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitiveDensity, OAI.SymmetricMahler.errorIntegrand

theorem OAI.SymmetricMahler.radial_primitive_uniform_small line 155

Source documentation

Uniform small error for every measurable angular fiber satisfying the proved sine condition. The threshold is independent of the basepoint and fiber.

theorem radial_primitive_uniform_small {ε : ℝ} (hε : 0 < ε) :
    ∃ m₀ : ℝ, ∀ m : ℝ, m₀ ≤ m → ∀ r₀ ∈ Ico (0 : ℝ) 1,
      ∀ θ : ℝ → ℝ, Measurable θ →
        (∀ r ∈ Ioo r₀ 1,
          sqrt ((1-r^2)*(radialMap r-radialMap r₀)/r) ≤ sin (θ r)) →
        ∀ s ∈ Ico r₀ 1,
          IntervalIntegrable (radialPrimitiveDensity θ m) volume r₀ s ∧
          (∫ r in r₀..s, radialPrimitiveDensity θ m r) < s^(2*m : ℝ)+ε := by
…

Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitiveDensity