English
A version of the divergence theorem valid under an equivariant coordinate change with a countable exceptional set.
Русский
Версия теоремы дивергенции при эквивариантном переходе координат, допускающая счетное множество исключений.
LaTeX
$$$\\text{integral_divergence_of_hasFDerivAt_off_countable_of_equiv}$$$
Lean4
/-- **Divergence theorem** for a family of functions `f : Fin (n + 1) → ℝⁿ⁺¹ → E`. See also
`MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable'` for a version formulated
in terms of a vector-valued function `f : ℝⁿ⁺¹ → Eⁿ⁺¹`. -/
theorem integral_divergence_of_hasFDerivAt_off_countable' (hle : a ≤ b) (f : Fin (n + 1) → ℝⁿ⁺¹ → E)
(f' : Fin (n + 1) → ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] E) (s : Set ℝⁿ⁺¹) (hs : s.Countable) (Hc : ∀ i, ContinuousOn (f i) (Icc a b))
(Hd : ∀ x ∈ (pi Set.univ fun i => Ioo (a i) (b i)) \ s, ∀ (i), HasFDerivAt (f i) (f' i x) x)
(Hi : IntegrableOn (fun x => ∑ i, f' i x (e i)) (Icc a b)) :
(∫ x in Icc a b, ∑ i, f' i x (e i)) =
∑ i : Fin (n + 1), ((∫ x in face i, f i (frontFace i x)) - ∫ x in face i, f i (backFace i x)) :=
integral_divergence_of_hasFDerivAt_off_countable a b hle (fun x i => f i x)
(fun x => ContinuousLinearMap.pi fun i => f' i x) s hs (continuousOn_pi.2 Hc)
(fun x hx => hasFDerivAt_pi.2 (Hd x hx)) Hi
