PrimitiveEquality.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.hasDerivAt_planarPrimitive_fiber line 13
Source documentation
Along the actual fiber, the original vertical primitive has exactly the radial density as derivative. This proves the substitution locally without assuming a change-of-variables identity.
```
theorem hasDerivAt_planarPrimitive_fiber {q r₀ r : ℝ} {m : ℕ}
    (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀) (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1)
    (hseg : ∀ t ∈ uIcc (0 : ℝ) (fiberHeight q r),
      (q : ℂ)+(t : ℂ)*Complex.I ∈ MahlerConformal.Omega) :
    HasDerivAt (fun s => planarPrimitive m q (fiberHeight q s))
      (radialPrimitiveDensity (fiberAngle q) (m : ℝ) r) r := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberHeight, OAI.MahlerConformal.Omega, OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.radialPrimitiveDensity, OAI.SymmetricMahler.fiberAngle

theorem OAI.SymmetricMahler.planarPrimitive_eq_radial_of_geometry line 35

Source documentation

Global radial substitution follows once the fiber's endpoint continuity and vertical-segment geometry have been established.

theorem planarPrimitive_eq_radial_of_geometry {q r₀ r : ℝ} {m : ℕ}
    (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀) (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1)
    (hheight : ContinuousOn (fiberHeight q) (Icc r₀ r))
    (hseg : ∀ s ∈ Icc r₀ r, ∀ t ∈ uIcc (0 : ℝ) (fiberHeight q s),
      (q : ℂ)+(t : ℂ)*Complex.I ∈ MahlerConformal.Omega) :
    planarPrimitive m q (fiberHeight q r) = radialPrimitive q r₀ (m : ℝ) r := by
…

Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberHeight, OAI.MahlerConformal.Omega, OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.radialPrimitive