FiberHeight.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.rotated_derivative_im line 10
Source documentation
The angular function B gives the imaginary part of the rotated complex derivative.
```
theorem rotated_derivative_im {r θ : ℝ} (hr : 0 < r) (hr1 : r < 1) :
    r*((deriv MahlerConformal.F (MahlerConformal.polar r θ))*
      Complex.exp ((θ : ℂ)*Complex.I)).im = MahlerConformal.B r θ := by
…
```
Mentions: OAI.MahlerConformal.F, OAI.MahlerConformal.polar, OAI.MahlerConformal.B
def OAI.SymmetricMahler.fiberHeight line 30
theorem OAI.SymmetricMahler.hasDerivAt_fiberHeight line 34
Source documentation
The actual chosen fiber has positive vertical derivative on its open domain.
```
theorem hasDerivAt_fiberHeight {q r : ℝ} (hr : r ∈ fiberDomain q) :
    HasDerivAt (fiberHeight q)
      (r*‖deriv MahlerConformal.F (MahlerConformal.polar r (fiberAngle q r))‖^2 /
        MahlerConformal.B r (fiberAngle q r)) r := by
…
```
Mentions: OAI.SymmetricMahler.fiberDomain, OAI.SymmetricMahler.fiberHeight, OAI.MahlerConformal.F, OAI.MahlerConformal.polar, OAI.SymmetricMahler.fiberAngle, OAI.MahlerConformal.B
theorem OAI.SymmetricMahler.deriv_fiberHeight_pos line 68
theorem OAI.SymmetricMahler.contDiffAt_fiberHeight line 77
theorem OAI.SymmetricMahler.strictMonoOn_fiberHeight line 85
Source documentation
Each constructed upper vertical fiber is traversed strictly upward.
```
theorem strictMonoOn_fiberHeight {q r₀ : ℝ} (hr₀ : 0 ≤ r₀)
    (hq : radialMap r₀ = |q|) : StrictMonoOn (fiberHeight q) (Ioo r₀ 1) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberHeight