PlanarIntegralRegularity.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.segmentPoint line 11
Source documentation
The fixed-interval parametrization of the entire vertical segment.
```
def segmentPoint (p : ℂ × ℝ) : ℂ := (p.1.re : ℂ) + (p.2 * p.1.im : ℝ) * I
```
def OAI.SymmetricMahler.segmentParameterDomain line 13
def OAI.SymmetricMahler.planarSegmentDomain line 15
lemma OAI.SymmetricMahler.contDiff_segmentPoint line 17
lemma OAI.SymmetricMahler.isOpen_segmentParameterDomain line 22
lemma OAI.SymmetricMahler.isOpen_planarSegmentDomain line 25
theorem OAI.SymmetricMahler.planarPrimitive_eq_fixedIntegral line 30
Source documentation
The exact original integral under t=s*xi; the equality also holds at xi=0 and for negative xi, using oriented interval integration.
```
theorem planarPrimitive_eq_fixedIntegral (m : ℕ) (u : ℂ) :
    planarPrimitive m u.re u.im =
      u.im * ∫ s in Icc (0 : ℝ) 1, planarDensity m (segmentPoint (u,s)) := by
…
```
Mentions: OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.planarDensity, OAI.SymmetricMahler.segmentPoint
lemma OAI.SymmetricMahler.contDiffOn_segmentDensity line 40
Source documentation
The density on the fixed interval is jointly smooth on its actual open domain.
```
lemma contDiffOn_segmentDensity (m : ℕ) :
    ContDiffOn ℝ ∞ (fun p => planarDensity m (segmentPoint p)) segmentParameterDomain := by
…
```
Mentions: OAI.SymmetricMahler.planarDensity, OAI.SymmetricMahler.segmentPoint, OAI.SymmetricMahler.segmentParameterDomain
theorem OAI.SymmetricMahler.contDiffOn_planarPrimitive_segment line 47
Source documentation
Joint C∞ regularity of the primitive on the open segment-containment domain, including its real diameter.
```
theorem contDiffOn_planarPrimitive_segment (m : ℕ) :
    ContDiffOn ℝ ∞ (fun u : ℂ => planarPrimitive m u.re u.im) planarSegmentDomain := by
…
```
Mentions: OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.planarSegmentDomain