ShellRegularity.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.coordClosedBall line 9
lemma OAI.MahlerStokes.continuous_radiusSq line 11
lemma OAI.MahlerStokes.isCompact_coordClosedBall line 14
lemma OAI.MahlerStokes.isCompact_closedShell line 24
lemma OAI.MahlerStokes.coordAnnulus_subset_shell line 30
lemma OAI.MahlerStokes.integrableOn_shell_annulus line 35
lemma OAI.MahlerStokes.radiusSq_boundary line 39

lemma OAI.MahlerStokes.integrable_boundary_difference line 48

Source documentation

Boundary integrability follows from ordinary continuity on the sphere.

lemma integrable_boundary_difference {n : ℕ} (i : Fin (n+1)) (R : ℝ)
    (f : (Fin (n+1) → ℝ) → ℝ) (hf : ContinuousOn f {x | radiusSq x = R^2}) :
    Integrable (fun y : Fin n → ℝ =>
      f (i.insertNth (chord R y) y) - f (i.insertNth (-chord R y) y)) := by
…

Mentions: OAI.MahlerStokes.radiusSq, OAI.MahlerStokes.chord

theorem OAI.MahlerStokes.integral_partial_annulus_of_C1 line 73

Source documentation

The annulus identity under local C1 assumptions only; integrability of both volume and boundary terms is proved, not assumed.

theorem integral_partial_annulus_of_C1 {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)) :
    (∫ 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.coordBall, OAI.MahlerStokes.chord

theorem OAI.MahlerStokes.integral_divergence_annulus_of_C1 line 90

Source documentation

Full divergence with the inner sphere oriented outward from its own ball. Its flux consequently occurs with a minus sign.

theorem integral_divergence_annulus_of_C1 {n : ℕ} {a R : ℝ} (haR : a^2 ≤ R^2)
    (F : Fin (n+1) → (Fin (n+1) → ℝ) → ℝ)
    (hF : ∀ i x, x ∈ closedShell (n+1) a R → DifferentiableAt ℝ (F i) x)
    (hD : ∀ i, ContinuousOn (fun x => fderiv ℝ (F i) x (Pi.single i 1)) (closedShell (n+1) a R)) :
    (∫ x in coordAnnulus (n+1) a R, ∑ i, fderiv ℝ (F i) x (Pi.single i 1)) =
      (∑ i, ∫ y in coordBall n R,
        F i (i.insertNth (chord R y) y) - F i (i.insertNth (-chord R y) y)) -
      ∑ i, ∫ y in coordBall n a,
        F i (i.insertNth (chord a y) y) - F i (i.insertNth (-chord a y) y) := by
…

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