InteriorStokes.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MahlerStokes.extDeriv_zero_off_tsupport line 10
theorem OAI.MahlerStokes.integral_partial_univ line 16

theorem OAI.MahlerStokes.integral_extDeriv_univ line 27

Source documentation

Stokes for a compactly supported form in the whole ambient space.

theorem integral_extDeriv_univ {n : ℕ}
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hω : ContDiff ℝ 1 ω) (hc : HasCompactSupport ω) :
    (∫ x, extDeriv ω x (coordinateBasis (n+1))) = 0 := by
…

Mentions: OAI.MahlerStokes.coordinateBasis

theorem OAI.MahlerStokes.integral_extDeriv_interior_support line 45

Source documentation

The actual interior patch contributes zero, since the support of the localized form stays strictly inside the domain.

theorem integral_extDeriv_interior_support {n : ℕ} {s : Set (Fin (n+1) → ℝ)}
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hω : ContDiff ℝ 1 ω) (hc : HasCompactSupport ω) (hs : tsupport ω ⊆ s) :
    (∫ x in s, extDeriv ω x (coordinateBasis (n+1))) = 0 := by
…

Mentions: OAI.MahlerStokes.coordinateBasis

theorem OAI.MahlerStokes.integral_extDeriv_boundary_patches line 57

Source documentation

Remove the interior term from the volume partition. All remaining terms are supported in boundary charts, before oriented chart transport.

theorem integral_extDeriv_boundary_patches {n : ℕ} {ι : Type*} [Fintype ι]
    {K W s : Set (Fin (n+1) → ℝ)}
    (ρ : SmoothPartitionOfUnity (Option ι) 𝓘(ℝ, Fin (n+1) → ℝ) (Fin (n+1) → ℝ) K)
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hW : IsOpen W) (hsW : s ⊆ W) (hs : MeasurableSet s)
    (hsum : ∀ x ∈ W, ∑ i, ρ i x = 1)
    (hρ : ∀ i, HasCompactSupport (ρ i))
    (hω : ∀ i, ∀ x ∈ tsupport (ρ i), ContDiffAt ℝ 1 ω x)
    (hinterior : tsupport (ρ none) ⊆ s) :
    (∫ x in s, extDeriv ω x (coordinateBasis (n+1))) =
      ∑ i : ι, ∫ x in s,
        extDeriv (fun z => ρ (some i) z • ω z) x (coordinateBasis (n+1)) := by
…

Mentions: OAI.MahlerStokes.coordinateBasis