OAI/Analysis/Mahler/RadialPrimitiveDeriv.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.radialPrimitive line 11
2. lemma OAI.SymmetricMahler.continuousAt_radialPrimitiveDensity line 14
3. lemma OAI.SymmetricMahler.measurable_radialPrimitiveDensity line 28
4. theorem OAI.SymmetricMahler.hasDerivAt_radialPrimitive line 36

   Source documentation

   The radial primitive has its defining density as derivative, including an integrable singular lower endpoint.

   theorem hasDerivAt_radialPrimitive {q r₀ m r : ℝ} (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀)
       (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) :
       HasDerivAt (radialPrimitive q r₀ m)
         (radialPrimitiveDensity (fiberAngle q) m r) r := by
   …

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

5. theorem OAI.SymmetricMahler.radial_density_div_vertical_speed line 48

   Source documentation

   Dividing radial density by vertical speed gives the prescribed vertical derivative.

   theorem radial_density_div_vertical_speed {q r m : ℝ} (hr : r ∈ fiberDomain q) :
       radialPrimitiveDensity (fiberAngle q) m r / deriv (fiberHeight q) r =
         (4*m/Real.pi)*r^(2*m-2 : ℝ) /
           ‖deriv MahlerConformal.F (MahlerConformal.polar r (fiberAngle q r))‖^2 := by
   …

   Mentions: OAI.SymmetricMahler.fiberDomain, OAI.SymmetricMahler.radialPrimitiveDensity, OAI.SymmetricMahler.fiberAngle, OAI.SymmetricMahler.fiberHeight, OAI.MahlerConformal.F, OAI.MahlerConformal.polar