ChartStokes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.orientedCoefficient line 12

Source documentation

Actual coefficient of an n-form in the oriented omitted-coordinate basis.

def orientedCoefficient {n : ℕ}
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (i : Fin (n+1)) (x : Fin (n+1) → ℝ) : ℝ :=
…

lemma OAI.MahlerStokes.contDiff_orientedCoefficient line 17
lemma OAI.MahlerStokes.extDeriv_eq_divergence line 25

theorem OAI.MahlerStokes.integral_extDeriv_box line 40

Source documentation

Coordinate Stokes on a box, for actual C1 differential forms.

theorem integral_extDeriv_box {n : ℕ} (a b : Fin (n+1) → ℝ) (hab : a ≤ b)
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hω : ContDiff ℝ 1 ω) :
    (∫ x in Icc a b, extDeriv ω x (coordinateBasis (n+1))) =
      ∑ i : Fin (n+1), (-1 : ℝ)^i.val *
        ((∫ y in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            ω (i.insertNth (b i) y) (i.removeNth (coordinateBasis (n+1)))) -
          ∫ y in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            ω (i.insertNth (a i) y) (i.removeNth (coordinateBasis (n+1)))) := by
…

Mentions: OAI.MahlerStokes.coordinateBasis

theorem OAI.MahlerStokes.integral_extDeriv_box_one_face line 69

Source documentation

Local boundary-chart Stokes after a cutoff kills all artificial faces. Only the selected physical boundary face contributes.

theorem integral_extDeriv_box_one_face {n : ℕ} (a b : Fin (n+1) → ℝ) (hab : a ≤ b)
    (k : Fin (n+1))
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hω : ContDiff ℝ 1 ω)
    (hback : ∀ i : Fin (n+1), ∀ y ∈ Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
      ω (i.insertNth (a i) y) (i.removeNth (coordinateBasis (n+1))) = 0)
    (hfront : ∀ i : Fin (n+1), i ≠ k → ∀ y ∈ Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
      ω (i.insertNth (b i) y) (i.removeNth (coordinateBasis (n+1))) = 0) :
    (∫ x in Icc a b, extDeriv ω x (coordinateBasis (n+1))) =
      (-1 : ℝ)^k.val * ∫ y in Icc (a ∘ k.succAbove) (b ∘ k.succAbove),
        ω (k.insertNth (b k) y) (k.removeNth (coordinateBasis (n+1))) := by
…

Mentions: OAI.MahlerStokes.coordinateBasis

theorem OAI.MahlerStokes.integral_pullback_extDeriv_box line 105

Source documentation

Stokes on a parametrized box. Every integrand is the actual pullback along φ, including its derivative and orientation. This is the local chart identity needed before assembling a compact regular sublevel.

theorem integral_pullback_extDeriv_box {n : ℕ} (a b : Fin (n+1) → ℝ) (hab : a ≤ b)
    (φ : (Fin (n+1) → ℝ) → E) (ω : E → E [⋀^Fin n]→L[ℝ] ℝ)
    (hφ : ContDiff ℝ 2 φ) (hω : Differentiable ℝ ω)
    (hpb : ContDiff ℝ 1 (pullbackForm φ ω)) :
    (∫ x in Icc a b,
      extDeriv ω (φ x) (fun i => fderiv ℝ φ x (coordinateBasis (n+1) i))) =
      ∑ i : Fin (n+1), (-1 : ℝ)^i.val *
        ((∫ y in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
          pullbackForm φ ω (i.insertNth (b i) y) (i.removeNth (coordinateBasis (n+1)))) -
        ∫ y in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
          pullbackForm φ ω (i.insertNth (a i) y) (i.removeNth (coordinateBasis (n+1)))) := by
…

Mentions: OAI.MahlerStokes.pullbackForm, OAI.MahlerStokes.coordinateBasis