CoordinateBall.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.radiusSq line 18
Source documentation
The squared Euclidean radius, in real coordinates with standard Lebesgue measure.
```
def radiusSq {n : ℕ} (x : Fin n → ℝ) : ℝ := ∑ i, x i ^ 2
```
def OAI.MahlerStokes.coordBall line 20
Source documentation
An actual Euclidean ball in coordinates; the ambient Pi norm is irrelevant.
```
def coordBall (n : ℕ) (R : ℝ) : Set (Fin n → ℝ) := {x | radiusSq x < R ^ 2}
```
Mentions: OAI.MahlerStokes.radiusSq
def OAI.MahlerStokes.chord line 21
lemma OAI.MahlerStokes.radiusSq_insertNth line 23
lemma OAI.MahlerStokes.measurableSet_coordBall line 29
lemma OAI.MahlerStokes.ball_slice line 33

theorem OAI.MahlerStokes.setIntegral_slice line 46

Source documentation

Fubini in the i-th coordinate, for an actual restricted Lebesgue integral.

theorem setIntegral_slice {n : ℕ} (i : Fin (n+1)) {s : Set (Fin (n+1) → ℝ)}
    (hs : MeasurableSet s) (f : (Fin (n+1) → ℝ) → ℝ) (hf : IntegrableOn f s) :
    (∫ x in s, f x) = ∫ y : Fin n → ℝ, ∫ t in {t | i.insertNth t y ∈ s}, f (i.insertNth t y) := by
…

lemma OAI.MahlerStokes.coordBall_subset_cube line 65
lemma OAI.MahlerStokes.integrableOn_coordBall line 74
lemma OAI.MahlerStokes.hasDerivAt_insertNth line 78

theorem OAI.MahlerStokes.integral_partial_coordBall line 94

Source documentation

Divergence for one component on an actual Euclidean ball, by integration along coordinate chords. Each boundary term is an ordinary Lebesgue integral on a hemisphere parameter domain; its sign is outward from the ball.

theorem integral_partial_coordBall {n : ℕ} (i : Fin (n+1)) (R : ℝ)
    (f : (Fin (n+1) → ℝ) → ℝ) (hf : Differentiable ℝ f)
    (hg : Continuous (fun x => fderiv ℝ f x (Pi.single i 1))) :
    (∫ x in coordBall (n+1) 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) := by
…

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

theorem OAI.MahlerStokes.integral_divergence_coordBall line 121

Source documentation

Actual divergence equals the sum of oriented hemisphere-coordinate fluxes.

theorem integral_divergence_coordBall {n : ℕ} (R : ℝ)
    (F : Fin (n+1) → (Fin (n+1) → ℝ) → ℝ)
    (hF : ∀ i, Differentiable ℝ (F i))
    (hD : ∀ i, Continuous (fun x => fderiv ℝ (F i) x (Pi.single i 1))) :
    (∫ x in coordBall (n+1) 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) := by
…

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