PlanarDensity.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.planarDensity line 12
Source documentation
The vertical primitive density, written with squared norms so smoothness at the zero is explicit for integral m.
```
noncomputable def planarDensity (m : ℕ) (u : ℂ) : ℝ :=
…
```
lemma OAI.SymmetricMahler.contDiffAt_normSq_comp line 16
theorem OAI.SymmetricMahler.contDiffAt_planarDensity line 23
Source documentation
Smoothness of the actual vertical density, including at the origin.
```
theorem contDiffAt_planarDensity (m : ℕ) {u : ℂ} (hu : u ∈ MahlerConformal.Omega) :
    ContDiffAt ℝ ∞ (planarDensity m) u := by
…
```
Mentions: OAI.MahlerConformal.Omega, OAI.SymmetricMahler.planarDensity
lemma OAI.SymmetricMahler.planarDensity_nonneg line 32
lemma OAI.SymmetricMahler.planarDensity_pos line 38
def OAI.SymmetricMahler.planarPrimitive line 48
Source documentation
The original vertical integral, before its equality with the radial integral.
```
noncomputable def planarPrimitive (m : ℕ) (q t : ℝ) : ℝ :=
…
```
lemma OAI.SymmetricMahler.continuousAt_planarDensity_vertical line 51
theorem OAI.SymmetricMahler.hasDerivAt_planarPrimitive line 62
Source documentation
The fundamental theorem yields the vertical derivative whenever the segment from zero lies in Omega. Segment containment is an explicit geometric premise.
```
theorem hasDerivAt_planarPrimitive (m : ℕ) {q t : ℝ}
    (hseg : ∀ s ∈ uIcc (0 : ℝ) t, (q : ℂ)+(s : ℂ)*Complex.I ∈ MahlerConformal.Omega) :
    HasDerivAt (planarPrimitive m q) (planarDensity m ((q : ℂ)+(t : ℂ)*Complex.I)) t := by
…
```
Mentions: OAI.MahlerConformal.Omega, OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.planarDensity

theorem OAI.SymmetricMahler.planarDensity_eq line 78

Source documentation

The polynomial expression equals the norm-power density.

theorem planarDensity_eq (m : ℕ) (hm : 1 ≤ m) (u : ℂ) :
    planarDensity m u = (4*(m : ℝ)/Real.pi)*
      ‖MahlerConformal.inverseF u‖^(2*(m : ℝ)-2 : ℝ)*
      ‖deriv MahlerConformal.inverseF u‖^2 := by
…

Mentions: OAI.SymmetricMahler.planarDensity, OAI.MahlerConformal.inverseF

theorem OAI.SymmetricMahler.hasDerivAt_actual_primitive_density line 94
Source documentation
Both the radial inverse-coordinate primitive and the original vertical integral have the same density on each upper fiber.
```
theorem hasDerivAt_actual_primitive_density {q r₀ r : ℝ} {m : ℕ}
    (hm : 2 ≤ m) (hr₀ : 0 ≤ r₀) (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) :
    HasDerivAt (fun t => radialPrimitive q r₀ (m : ℝ) (verticalRadius q t))
      (planarDensity m ((q : ℂ)+(fiberHeight q r : ℂ)*Complex.I)) (fiberHeight q r) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.radialPrimitive, OAI.SymmetricMahler.verticalRadius, OAI.SymmetricMahler.planarDensity, OAI.SymmetricMahler.fiberHeight
lemma OAI.SymmetricMahler.planarPrimitive_zero line 101
lemma OAI.SymmetricMahler.planarPrimitive_nonneg line 104
theorem OAI.SymmetricMahler.strictMonoOn_planarPrimitive line 110
Source documentation
Positivity away from the single zero is sufficient for strict increase on an entire vertical interval, including intervals crossing the origin.
```
theorem strictMonoOn_planarPrimitive {m : ℕ} (hm : 0 < m) {q l u : ℝ}
    (hl : l < 0) (hu : 0 < u)
    (hOmega : ∀ t ∈ Ioo l u, (q : ℂ)+(t : ℂ)*Complex.I ∈ MahlerConformal.Omega) :
    StrictMonoOn (planarPrimitive m q) (Ioo l u) := by
…
```
Mentions: OAI.MahlerConformal.Omega, OAI.SymmetricMahler.planarPrimitive