OAI/Analysis/Mahler/HalfspaceStokes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerStokes.lowerHalfspace line 11
2. lemma OAI.MahlerStokes.measurableSet_lowerHalfspace line 13
3. lemma OAI.MahlerStokes.slice_eq_update line 17
4. lemma OAI.MahlerStokes.contDiff_slice line 23
5. lemma OAI.MahlerStokes.hasCompactSupport_slice line 28
6. lemma OAI.MahlerStokes.integral_partial_slice_Iio line 35
7. lemma OAI.MahlerStokes.integral_partial_slice_zero line 48
8. theorem OAI.MahlerStokes.integral_partial_lowerHalfspace line 66

   Source documentation

   Coordinate divergence through a flat boundary. Transverse derivatives integrate to zero; the k derivative gives the upper face with positive sign.

   theorem integral_partial_lowerHalfspace {n : ℕ} (i k : Fin (n+1)) (R : ℝ)
       {f : (Fin (n+1) → ℝ) → ℝ} (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
       (∫ x in lowerHalfspace k R, fderiv ℝ f x (Pi.single i 1)) =
         if i = k then ∫ y : Fin n → ℝ, f (k.insertNth R y) else 0 := by
   …

   Mentions: OAI.MahlerStokes.lowerHalfspace

9. theorem OAI.MahlerStokes.integral_extDeriv_lowerHalfspace line 100

   Source documentation

   Stokes on a coordinate half-space for an actual compactly supported C1 form. The boundary uses the outward orientation, including (-1)^k.

   theorem integral_extDeriv_lowerHalfspace {n : ℕ} (k : Fin (n+1)) (R : ℝ)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiff ℝ 1 ω) (hc : HasCompactSupport ω) :
       (∫ x in lowerHalfspace k R, extDeriv ω x (coordinateBasis (n+1))) =
         (-1 : ℝ)^k.val * ∫ y : Fin n → ℝ,
           ω (k.insertNth R y) (k.removeNth (coordinateBasis (n+1))) := by
   …

   Mentions: OAI.MahlerStokes.lowerHalfspace, OAI.MahlerStokes.coordinateBasis