CoordinateAnnulus.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.closedShell line 11
Source documentation
The closed annulus is used only for local differentiability and continuity.
```
def closedShell (n : ℕ) (a R : ℝ) : Set (Fin n → ℝ) :=
…
```

theorem OAI.MahlerStokes.integral_punctured_chord line 16

Source documentation

Fundamental theorem of calculus on a punctured chord. No regularity is required in the deleted middle interval.

theorem integral_punctured_chord {a A : ℝ} (ha : 0 ≤ a) (hA : a ≤ A)
    (f g : ℝ → ℝ)
    (hl : ∀ t ∈ Icc (-A) (-a), HasDerivAt f (g t) t)
    (hr : ∀ t ∈ Icc a A, HasDerivAt f (g t) t)
    (hgl : IntervalIntegrable g volume (-A) (-a))
    (hgr : IntervalIntegrable g volume a A) :
    (∫ t in Ioo (-A) A \ Ioo (-a) a, g t) =
      (f A - f (-A)) - (f a - f (-a)) := by
…

lemma OAI.MahlerStokes.chord_mono line 51
lemma OAI.MahlerStokes.chord_shell line 54
def OAI.MahlerStokes.coordAnnulus line 80
Source documentation
Open-ball puncture; the inner sphere has zero volume.
```
def coordAnnulus (n : ℕ) (a R : ℝ) : Set (Fin n → ℝ) :=
…
```
lemma OAI.MahlerStokes.boundary_difference_zero line 83
lemma OAI.MahlerStokes.integral_boundary_difference line 90

theorem OAI.MahlerStokes.integral_partial_coordAnnulus line 104

Source documentation

Divergence for one component on an annulus. Differentiability and continuity of the actual partial derivative are required only on its closed shell, so a singularity anywhere inside the hole is permitted.

theorem integral_partial_coordAnnulus {n : ℕ} (i : Fin (n+1)) {a R : ℝ}
    (haR : a^2 ≤ R^2) (f : (Fin (n+1) → ℝ) → ℝ)
    (hf : ∀ x ∈ closedShell (n+1) a R, DifferentiableAt ℝ f x)
    (hg : ContinuousOn (fun x => fderiv ℝ f x (Pi.single i 1)) (closedShell (n+1) a R))
    (hgi : IntegrableOn (fun x => fderiv ℝ f x (Pi.single i 1)) (coordAnnulus (n+1) a R))
    (hbR : Integrable (fun y : Fin n → ℝ =>
      f (i.insertNth (chord R y) y) - f (i.insertNth (-chord R y) y)))
    (hba : Integrable (fun y : Fin n → ℝ =>
      f (i.insertNth (chord a y) y) - f (i.insertNth (-chord a y) y))) :
    (∫ x in coordAnnulus (n+1) a R, fderiv ℝ f x (Pi.single i 1)) =
      (∫ y in coordBall n R, f (i.insertNth (chord R y) y) - f (i.insertNth (-chord R y) y)) -
      ∫ y in coordBall n a, f (i.insertNth (chord a y) y) - f (i.insertNth (-chord a y) y) := by
…

Mentions: OAI.MahlerStokes.closedShell, OAI.MahlerStokes.coordAnnulus, OAI.MahlerStokes.chord, OAI.MahlerStokes.coordBall