MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable'
theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable' :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {n : ℕ}
(a b : Fin (n + 1) → ℝ),
a ≤ b →
∀ (f : Fin (n + 1) → (Fin (n + 1) → ℝ) → E) (f' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E)
(s : Set (Fin (n + 1) → ℝ)),
s.Countable →
(∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)) →
(∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x) →
MeasureTheory.IntegrableOn (fun x => Finset.univ.sum fun i => (f' i x) (Pi.single i 1)) (Set.Icc a b)
MeasureTheory.volume →
(∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, Finset.univ.sum fun i => (f' i x) (Pi.single i 1)) =
Finset.univ.sum fun i =>
(∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (b i) x)) -
∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (a i) x)
This theorem is a version of the **Divergence Theorem** for a family of functions `f : Fin (n + 1) → ℝⁿ⁺¹ → E`. Given a natural number `n` and two functions `a, b : Fin (n + 1) → ℝ` such that `a ≤ b`, a family of functions `f` and their derivatives `f'`, and a countable set `s`, the theorem states that if each function `f i` is continuous on the interval `[a, b]`, and each function `f i` has `f' i x` as its derivative at each point `x` in the open interval `(a, b)` excluding `s`, and if the function that sums up the derivatives scaled by the indicator function `Pi.single i 1` is integrable on `[a, b]`, then the integral of this sum over `[a, b]` equals the sum, over all `i`, of the difference between the integrals of `f i` at `b` and `a`, projected onto the smaller dimensional space by `i.insertNth`. Each integral is taken over the smaller dimensional interval `[a ∘ i.succAbove, b ∘ i.succAbove]`. This theorem is an essential tool in vector calculus and physical sciences.
More concisely: The Divergence Theorem for a family of functions `f : Fin (n + 1) → ℝⁿ⁺¹ → E` states that if each `f i` is continuous on `[a, b]`, has `f' i x` as its derivative at each `x ∈ (a, b) \ s`, and the sum of derivatives scaled by the indicator functions is integrable, then the integral of the sum equals the sum of the integrals of `f i` over the smaller dimensional intervals from `a` to `b` along the corresponding axes.
|
MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le
theorem MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f g : ℝ × ℝ → E)
(f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a b : ℝ × ℝ),
a ≤ b →
∀ (s : Set (ℝ × ℝ)),
s.Countable →
ContinuousOn f (Set.Icc a b) →
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x) →
(∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x) →
MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b)
MeasureTheory.volume →
∫ (x : ℝ × ℝ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) =
(((∫ (x : ℝ) in a.1 ..b.1, g (x, b.2)) - ∫ (x : ℝ) in a.1 ..b.1, g (x, a.2)) +
∫ (y : ℝ) in a.2 ..b.2, f (b.1, y)) -
∫ (y : ℝ) in a.2 ..b.2, f (a.1, y)
The **Divergence theorem** for functions on the plane along rectangles states that for two functions `f` and `g` mapping from ℝ² to a complete normed additive commutative group `E`, given derivatives `f'` and `g'`, and a rectangle defined by `a` and `b` (where `a ≤ b`) in ℝ², if `f` and `g` are continuous on the rectangle, and `f` and `g` have their derivatives almost everywhere inside the rectangle (excluding a countable set `s`), then the integral over the rectangle of the divergence of the derivative vector `(f' x, g' x)` equals the net flux of `f` and `g` through the boundary of the rectangle. The divergence is defined here as `(f' x) (1, 0) + (g' x) (0, 1)`. The net flux is calculated as the integral of `g` over the top and bottom edges of the rectangle, minus the integral of `f` over the left and right edges of the rectangle. This theorem is a fundamental result in vector calculus.
More concisely: The Divergence theorem in the plane states that the integral of the divergence of a continuously differentiable vector field's derivative over a rectangle equals the net flux of the field through the rectangle's boundary.
|
MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁
theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {n : ℕ}
(I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E)
(f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E) (s : Set (Fin (n + 1) → ℝ)),
s.Countable →
ContinuousOn f (BoxIntegral.Box.Icc I) →
(∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) →
MeasureTheory.IntegrableOn (fun x => Finset.univ.sum fun i => (f' x) (Pi.single i 1) i)
(BoxIntegral.Box.Icc I) MeasureTheory.volume →
(∫ (x : Fin (n + 1) → ℝ) in BoxIntegral.Box.Icc I, Finset.univ.sum fun i => (f' x) (Pi.single i 1) i) =
Finset.univ.sum fun i =>
(∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i
This theorem, `MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁`, states that for any normed add commutative group `E`, any complete normed space over real numbers `ℝ` with underlying type `E`, a natural number `n`, a box integral `I` in `n+1` dimensions, a function `f` mapping from `ℝ` in `n+1` dimensions to `E` in `n+1` dimensions, its derivative `f'`, and a countable set `s` in `ℝ` in `n+1` dimensions, if `f` is continuous on the closed box `I`, and at every point within `I` excluding `s`, `f` has its derivative within `I`, then if the integral of the pointwise norm of `f'` over the closed box `I` is finite, the integral over the box `I` of the sum over all elements in the universe finite set of the function `f'` applied to the function `Pi.single i 1` is equal to the sum over all elements in the universe finite set of the difference between the integral over the face of box `I` at upper and lower limits of `f` applied to the function inserting the upper or lower bound at `i` position, respectively.
More concisely: If a function `f` from `ℝ^(n+1)` to a Banach space `E` is continuous on a closed box `I` and has a derivative within `I` at all points except for a countable set `s`, and the integral of the norm of `f'` over `I` is finite, then the integral of `f'` over `I` equals the sum of the integrals of `f` over the faces of `I` at upper and lower limits, for all `i`, for the points in `s`.
|
MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable
theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f f' : ℝ → E)
{a b : ℝ} {s : Set ℝ},
s.Countable →
ContinuousOn f (Set.uIcc a b) →
(∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x) →
IntervalIntegrable f' MeasureTheory.volume a b → ∫ (x : ℝ) in a..b, f' x = f b - f a
The Fundamental Theorem of Calculus, Part 2, states that for a function `f` mapping real numbers to a normed group with a normed real vector space structure and a complete metric space structure. Given two real numbers `a` and `b`, and a countable set `s`, if `f` is continuous on the closed interval from `a` to `b`, `f` has a derivative at every point in the open interval from `min(a,b)` to `max(a,b)` excluding the points in `s`, and the derivative of `f` is interval integrable over `a` to `b` with respect to the Lebesgue measure, then the integral over `a` to `b` of the derivative of `f` equals `f(b) - f(a)`. This version of the theorem does not require `f` to be differentiable on the points in `s`, making it a more general form. Another version of the theorem requires `f` to be right differentiable.
More concisely: If a real-valued function `f` on a closed interval is continuous, has a derivative at almost all points, and its derivative is integrable, then the integral of the derivative equals the difference of the function values at the endpoints.
|
MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂
theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {n : ℕ}
(I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E)
(f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E) (s : Set (Fin (n + 1) → ℝ)),
s.Countable →
ContinuousOn f (BoxIntegral.Box.Icc I) →
(∀ x ∈ BoxIntegral.Box.Ioo I \ s, HasFDerivAt f (f' x) x) →
MeasureTheory.IntegrableOn (fun x => Finset.univ.sum fun i => (f' x) (Pi.single i 1) i)
(BoxIntegral.Box.Icc I) MeasureTheory.volume →
(∫ (x : Fin (n + 1) → ℝ) in BoxIntegral.Box.Icc I, Finset.univ.sum fun i => (f' x) (Pi.single i 1) i) =
Finset.univ.sum fun i =>
(∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i
This theorem, `MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂`, is an auxiliary part of a more extensive theorem in Measure Theory about the divergence of an integral when the function `f` has a derivative `f'` at points off a countable set `s` within a box `I` in a multidimensional real space.
It says that for any `n`-dimensional box `I` and a function `f` that maps a set of `n+1` real numbers to `n+1` vectors in a complete normed additive commutative group `E`, and its derivative `f'`, if `f` is continuous on the closed box `I` and for any point `x` in the open box but not in the set `s`, `f` has derivative `f'` at point `x`, then, given the integral of the sum of the application of `f'` at every point `x` to the function `Pi.single i 1` for every `i` in the universal finite set is finite on the closed box `I`, the integral over the closed box `I` of this sum equals the sum over each `i` in the universal finite set of the difference between the integrals of the function `f` applied to the function `i.insertNth (I.upper i) x` at point `i` and the function `f` applied to the function `i.insertNth (I.lower i) x` at point `i`, both integrals over a `n`-dimensional closed box that corresponds to the face `i` of the `n+1`-dimensional box `I`. In simple terms, it provides an expression for the divergence of the integral of a function in terms of the integrals over the faces of the box.
This theorem is an intermediate step in proving a more complex statement about the divergence of integrals of functions with derivatives at certain points in Measure Theory, and it drops the assumption of differentiability on the boundary of the box compared to similar previous theorems.
More concisely: Given an `n`-dimensional box `I`, a continuous function `f` mapping `n+1` real numbers to vectors in a complete normed additive commutative group `E` with derivative `f'` at points in `I` excluding a countable set `s`, if the integral of the sum of `f'` applied to the `i`th coordinate function at each point in `I` is finite, then the integral over `I` of this sum equals the sum over `i` in the universal finite set of the difference between the integrals of `f` over the `i`th face of `I`.
|
MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable_of_le
theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable_of_le :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f f' : ℝ → E)
{a b : ℝ},
a ≤ b →
∀ {s : Set ℝ},
s.Countable →
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x) →
IntervalIntegrable f' MeasureTheory.volume a b → ∫ (x : ℝ) in a..b, f' x = f b - f a
This theorem, known as the "Fundamental theorem of calculus, part 2", posits that if a function `f`, which maps real numbers to elements of a complete normed space `E`, is continuous on a closed interval [a, b] and differentiable on the open interval (a, b) with the exception of a countable set `s`, then the integral of the derivative `f'` with respect to the Lebesgue measure (denoted as `MeasureTheory.volume`) over the interval from `a` to `b` is equal to the difference `f(b) - f(a)`. This version of the theorem assumes that `a` is less than or equal to `b`. The theorem also requires that `f'` be interval integrable over the interval from `a` to `b`.
More concisely: If a real-valued function `f` on a closed interval [a, b] is continuous on [a, b], differentiable on (a, b) except for a countable set, and its derivative `f'` is Lebesgue integrable on [a, b], then `∫(a, b) f'(x) dx = f(b) - f(a)`.
|
MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable
theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {n : ℕ}
(a b : Fin (n + 1) → ℝ),
a ≤ b →
∀ (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E)
(s : Set (Fin (n + 1) → ℝ)),
s.Countable →
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x) →
MeasureTheory.IntegrableOn (fun x => Finset.univ.sum fun i => (f' x) (Pi.single i 1) i) (Set.Icc a b)
MeasureTheory.volume →
(∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, Finset.univ.sum fun i => (f' x) (Pi.single i 1) i) =
Finset.univ.sum fun i =>
(∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i
This theorem is a formalization of the **Divergence Theorem** for Bochner integrals. The theorem states that for a function `f : ℝⁿ⁺¹ → Eⁿ⁺¹` which is continuous on a rectangular box `[a, b] : Set ℝⁿ⁺¹`, `a ≤ b`, and differentiable on its interior with derivative `f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹`. If the divergence `fun x ↦ ∑ i, f' x eᵢ i` is integrable on `[a, b]`, where `eᵢ = Pi.single i 1` is the `i`-th basis vector, then the integral of the divergence over the box is equal to the sum of integrals of `f` over the faces of the box, with appropriate signs depending on the face.
This result also holds if the function is not differentiable at countably many points in the interior of the box. The faces `x i = a i` and `x i = b i` of the box are represented as `face i = [a ∘ Fin.succAbove i, b ∘ Fin.succAbove i]` in `ℝⁿ`, where `Fin.succAbove : 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 ∘ backFace i` and `f ∘ frontFace i`, where `backFace i = Fin.insertNth i (a i)` and `frontFace i = Fin.insertNth i (b i)` are embeddings `ℝⁿ → ℝⁿ⁺¹` that insert `a i` (or `b i`) as `i`-th coordinate.
More concisely: The Divergence Theorem for Bochner integrals asserts that the integral of the divergence of a continuous, differentiable vector field over a rectangular box equals the sum of integrals of the field over the faces, with appropriate signs, provided the divergence is integrable.
|