Fubini's theorem to Divergence theorem

TheoremFubini's theorem#

Fubini's Theorem: For integrable functions on α × β, the Bochner integral of f is equal to the iterated Bochner integral. integrable_prod_iff can be useful to show that the function in question in integrable. MeasureTheory.Integrable.integral_prod_right is useful to show that the inner integral of the right-hand side is integrable.

MeasureTheory.integral_prod.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {E : Type u_3}
  [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ] (f : α × β → E) (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
Sources
MathlibMeasureTheory.integral_prod
Uses 13 · Used by 3
Statement usesAssociative algebra over a commutative ring · Bochner integral · Carathéodory's theorem (measure theory) · Giry monad · Measurable function
Proof usesApproximation by step functions · Completeness of R · Hausdorff space · Inner product space, over \(R\) or \(C\) · Metric structure · Pointwise convergence · Squeeze theorem · Topological module
Used byBuffon Needle Problem · Mean of product of independent random variables · Fernique's theorem

DefinitionProduct of finitely many measures#

Measure.pi μ is the finite product of the measures {μ i | i : ι}. It is defined to be measure corresponding to MeasureTheory.OuterMeasure.pi.

MeasureTheory.Measure.pi.{u_1, u_3} {ι : Type u_1} {α : ι → Type u_3} [Fintype ι]
  [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) :
  MeasureTheory.Measure ((i : ι) → α i)
Sources
MathlibMeasureTheory.Measure.pi
Uses 3 · Used by 2
Statement usesCarathéodory's theorem (measure theory) · Positive measure · Product of sigma-algebras
Used byDivergence theorem · Binomial law

DefinitionConvolution#

The convolution of two functions f and g with respect to a continuous bilinear map L and measure μ. It is defined to be (f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ.

MeasureTheory.convolution.{u𝕜, uG, uE, uE', uF} {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE}
  {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E']
  [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E']
  [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedSpace ℝ F] [Sub G] (f : G → E) (g : G → E')
  (L : E →L[𝕜] E' →L[𝕜] F) (μ : MeasureTheory.Measure G := by volume_tac) : G → F
Sources
MathlibMeasureTheory.convolution
Uses 1 · Used by 2
Statement usesBochner integral
Used byApproximation by convolution · Regularization by convolution

TheoremApproximation by convolution#

(φ i ⋆ g i) (k i) tends to z₀ as i tends to some filter l if * φ is a sequence of normed bump functions such that (φ i).rOut tends to 0 as i tends to l; * g i is μ-a.e. strongly measurable as i tends to l; * g i x tends to z₀ as (i, x) tends to l ×ˢ 𝓝 x₀; * k i tends to x₀.

ContDiffBump.convolution_tendsto_right.{uG, uE', u_1} {G : Type uG} {E' : Type uE'}
  [NormedAddCommGroup E'] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E']
  [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace E'] [BorelSpace G] [FiniteDimensional ℝ G]
  [μ.IsAddHaarMeasure] {ι : Type u_1} {φ : ι → ContDiffBump 0} {g : ι → G → E'} {k : ι → G} {x₀ : G}
  {z₀ : E'} {l : Filter ι} (hφ : Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0))
  (hig : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ)
  (hcg : Filter.Tendsto (Function.uncurry g) (l ×ˢ nhds x₀) (nhds z₀))
  (hk : Filter.Tendsto k l (nhds x₀)) :
  Filter.Tendsto
    (fun i =>
      MeasureTheory.convolution ((φ i).normed μ) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) μ (k i))
    l (nhds z₀)
Sources
MathlibContDiffBump.convolution_tendsto_right
Uses 12
Statement usesAlgebra of endomorphisms of a vector space · Ball · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Compactness in terms of filters · Convolution · Finite-dimensionality · Inner product space, over \(R\) or \(C\) · Measurable function · Radius of convergence
Proof usesCompleteness of R · Heine-Borel theorem (finite-dimensional normed spaces are proper)

TheoremRegularization by convolution#

Mathlib states this as HasCompactSupport.contDiff_convolution_left.

HasCompactSupport.contDiff_convolution_left.{u𝕜, uG, uE, uE', uF} {𝕜 : Type u𝕜} {G : Type uG}
  {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E']
  [NormedAddCommGroup F] {f : G → E} {g : G → E'} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E']
  [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G]
  [NormedSpace 𝕜 G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [μ.IsAddLeftInvariant]
  [μ.IsNegInvariant] {n : ℕ∞} (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 (↑n) f)
  (hg : MeasureTheory.LocallyIntegrable g μ) : ContDiff 𝕜 (↑n) (MeasureTheory.convolution f g L μ)
Sources
MathlibHasCompactSupport.contDiff_convolution_left
Uses 17
Statement uses\(C^k\) function · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Compactness in terms of filters · Convolution · Measurable function
Proof usesCharacteristic zero · Derivative of a composition of functions (Analysis) · Differentials (linear tangent functions) · Hausdorff space · Holomorphic functions · Homeomorphisms · Inner product space, over \(R\) or \(C\) · Product of vector spaces · Topology of a metric space · Topology on a normed vector space

TheoremChange of variables formula#

Change of variable formula for differentiable functions: if a function f is injective and differentiable on a measurable set s, then the Bochner integral of a function g : E → F on f '' s coincides with the integral of |(f' x).det| • g ∘ f on s.

MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E}
  [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure]
  (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s)
  (g : E → F) : ∫ (x : E) in f '' s, g x ∂μ = ∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ
Sources
MathlibMeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul
Uses 17 · Used by 2
Statement usesBochner integral · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Compactness in terms of filters · Determinant of endomorphisms · Finite-dimensionality · Measurable function
Proof usesBesicovitch covering theorem · Euclidean affine space · Euclidean domain · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Holomorphic functions · Invertibility · Lebesgue's density theorem · Pointwise convergence · The Triangle Inequality · Uniformly continuous function
Used byMellin inversion theorem · Change of variables to polar co-ordinates

TheoremDivergence theorem#

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 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 its integral is equal to the sum of integrals of f over the faces of [a, b], taken with appropriate 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.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 take y : ℝⁿ and insert a i (resp., b i) as i-th coordinate.

MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable.{u} {E : Type u}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ) (hle : 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) → ℝ))
  (hs : s.Countable) (Hc : ContinuousOn f (Set.Icc a b))
  (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x)
  (Hi :
    MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (Set.Icc a b)
      MeasureTheory.volume) :
  ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (Pi.single i 1) i =
    ∑ 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)
Sources
MathlibMeasureTheory.integral_divergence_of_hasFDerivAt_off_countable
Uses 13 · Used by 1
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Differentiable function between normed vector spaces · Lebesgue measure (Measures and integral calculus)
Proof usesAlgebra of endomorphisms of a vector space · Approximation by step functions · Hausdorff space · Heine-Cantor theorem · Metric structure · Pointwise convergence · Product of finitely many measures · Riemann sums · Topology of a metric space
Used byCauchy formulas

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.