PlanarRegularity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SymmetricMahler.vertical_segment_mem_Omega_regularity line 11
theorem OAI.SymmetricMahler.planarSegmentDomain_eq_Omega line 22
Source documentation
The open domain used for parameter integration is exactly Omega.
```
theorem planarSegmentDomain_eq_Omega : planarSegmentDomain = Omega := by
…
```
Mentions: OAI.SymmetricMahler.planarSegmentDomain
theorem OAI.SymmetricMahler.contDiffOn_planarPrimitive line 36
Source documentation
Full joint real C∞ regularity of P_m on all of Omega. In particular, no exclusion of the zero or xi=0 is needed.
```
theorem contDiffOn_planarPrimitive (m : ℕ) :
    ContDiffOn ℝ ∞ (fun u : ℂ => planarPrimitive m u.re u.im) Omega := by
…
```
Mentions: OAI.SymmetricMahler.planarPrimitive
theorem OAI.SymmetricMahler.contDiffAt_planarPrimitive line 41
theorem OAI.SymmetricMahler.contDiffOn_one_planarPrimitive line 45
theorem OAI.SymmetricMahler.differentiableOn_planarPrimitive line 49
theorem OAI.SymmetricMahler.continuousOn_fderiv_planarPrimitive line 55
Source documentation
Continuity of the full real Frechet derivative, for the real Jacobian and chain rule.
```
theorem continuousOn_fderiv_planarPrimitive (m : ℕ) :
    ContinuousOn (fderiv ℝ (fun u : ℂ => planarPrimitive m u.re u.im)) Omega :=
…
```
Mentions: OAI.SymmetricMahler.planarPrimitive
theorem OAI.SymmetricMahler.hasFDerivAt_planarPrimitive line 59
theorem OAI.SymmetricMahler.hasDerivAt_planarPrimitive_Omega line 65
Source documentation
The exact vertical FTC derivative on Omega, with no remaining segment premise.
```
theorem hasDerivAt_planarPrimitive_Omega (m : ℕ) {q t : ℝ}
    (hu : (q : ℂ)+(t : ℂ)*I ∈ Omega) :
    HasDerivAt (planarPrimitive m q)
      (planarDensity m ((q : ℂ)+(t : ℂ)*I)) t := by
…
```
Mentions: OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.planarDensity

theorem OAI.SymmetricMahler.hasDerivAt_planarPrimitive_source line 74

Source documentation

The vertical derivative formula for the planar primitive.

theorem hasDerivAt_planarPrimitive_source {m : ℕ} (hm : 2 ≤ m) {q t : ℝ}
    (hu : (q : ℂ)+(t : ℂ)*I ∈ Omega) :
    HasDerivAt (planarPrimitive m q)
      ((4*(m : ℝ)/Real.pi)*‖inverseF ((q : ℂ)+(t : ℂ)*I)‖^(2*(m : ℝ)-2 : ℝ)*
        ‖deriv inverseF ((q : ℂ)+(t : ℂ)*I)‖^2) t := by
…

Mentions: OAI.SymmetricMahler.planarPrimitive

theorem OAI.SymmetricMahler.contDiffOn_planarPrimitive_coordinates line 82

Source documentation

Joint smoothness in the two real coordinates.

theorem contDiffOn_planarPrimitive_coordinates (m : ℕ) :
    ContDiffOn ℝ ∞ (fun p : ℝ × ℝ => planarPrimitive m p.1 p.2)
      {p : ℝ × ℝ | (p.1 : ℂ)+(p.2 : ℂ)*I ∈ Omega} := by
…

Mentions: OAI.SymmetricMahler.planarPrimitive

theorem OAI.SymmetricMahler.planar_primitive_regularity line 93

Source documentation

Smoothness and the vertical derivative formula, for m >= 2.

theorem planar_primitive_regularity {m : ℕ} (hm : 2 ≤ m) :
    ContDiffOn ℝ ∞ (fun u : ℂ => planarPrimitive m u.re u.im) Omega ∧
    ContDiffOn ℝ 1 (fun u : ℂ => planarPrimitive m u.re u.im) Omega ∧
    (∀ q t : ℝ, (q : ℂ)+(t : ℂ)*I ∈ Omega →
      HasDerivAt (planarPrimitive m q)
        ((4*(m : ℝ)/Real.pi)*‖inverseF ((q : ℂ)+(t : ℂ)*I)‖^(2*(m : ℝ)-2 : ℝ)*
          ‖deriv inverseF ((q : ℂ)+(t : ℂ)*I)‖^2) t) :=
…

Mentions: OAI.SymmetricMahler.planarPrimitive