An auxiliary lemma for measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable. This is exactly box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at reformulated for the Bochner integral.

An auxiliary lemma for measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable. Compared to the previous lemma, here we drop the assumption of differentiability on the boundary of the box.

Divergence theorem for Bochner integral. If f : ℝⁿ⁺¹ → Eⁿ⁺¹ is continuous on a rectangular box [a, b] : set ℝⁿ⁺¹, a ≤ b, is differentiable on its interior with derivative f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹ and the divergence λ x, ∑ i, f' x eᵢ i is integrable on [a, b], where eᵢ = pi.single i 1 is the i-th basis vector, then its integral is equal to the sum of integrals of f over the faces of [a, b], taken with appropriat signs.

Moreover, the same is true if the function is not differentiable at countably many points of the interior of [a, b].

We represent both faces x i = a i and x i = b i as the box face i = [a ∘ fin.succ_above i, b ∘ fin.succ_above i] in ℝⁿ, where fin.succ_above : fin n ↪o fin (n + 1) is the order embedding with range {i}ᶜ. The restrictions of f : ℝⁿ⁺¹ → Eⁿ⁺¹ to these faces are given by f ∘ back_face i and f ∘ front_face i, where back_face i = fin.insert_nth i (a i) and front_face i = fin.insert_nth i (b i) are embeddings ℝⁿ → ℝⁿ⁺¹ that take y : ℝⁿ and insert a i (resp., b i) as i-th coordinate.

Divergence theorem for a family of functions f : fin (n + 1) → ℝⁿ⁺¹ → E. See also measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable' for a version formulated in terms of a vector-valued function f : ℝⁿ⁺¹ → Eⁿ⁺¹.

An auxiliary lemma that is used to specialize the general divergence theorem to spaces that do not have the form fin n → ℝ.

Fundamental theorem of calculus, part 2. This version assumes that f is continuous on the interval and is differentiable off a countable set s.

See also

• interval_integral.integral_eq_sub_of_has_deriv_right_of_le for a version that only assumes right differentiability of f;

• measure_theory.integral_eq_of_has_deriv_within_at_off_countable for a version that works both for a ≤ b and b ≤ a at the expense of using unordered intervals instead of set.Icc.

Fundamental theorem of calculus, part 2. This version assumes that f is continuous on the interval and is differentiable off a countable set s.

See also measure_theory.interval_integral.integral_eq_sub_of_has_deriv_right for a version that only assumes right differentiability of f.

Divergence theorem for functions on the plane along rectangles. It is formulated in terms of two functions f g : ℝ × ℝ → E and an integral over Icc a b = [a.1, b.1] × [a.2, b.2], where a b : ℝ × ℝ, a ≤ b. When thinking of f and g as the two coordinates of a single function F : ℝ × ℝ → E × E and when E = ℝ, this is the usual statement that the integral of the divergence of F inside the rectangle equals the integral of the normal derivative of F along the boundary.

See also measure_theory.integral2_divergence_prod_of_has_fderiv_within_at_off_countable for a version that does not assume a ≤ b and uses iterated interval integral instead of the integral over Icc a b.

Divergence theorem for functions on the plane. It is formulated in terms of two functions f g : ℝ × ℝ → E and iterated integral ∫ x in a₁..b₁, ∫ y in a₂..b₂, _, where a₁ a₂ b₁ b₂ : ℝ. When thinking of f and g as the two coordinates of a single function F : ℝ × ℝ → E × E and when E = ℝ, this is the usual statement that the integral of the divergence of F inside the rectangle with vertices (aᵢ, bⱼ), i, j =1,2, equals the integral of the normal derivative of F along the boundary.

See also measure_theory.integral_divergence_prod_Icc_of_has_fderiv_within_at_off_countable_of_le for a version that uses an integral over Icc a b, where a b : ℝ × ℝ, a ≤ b.