Theorems · Theorem · real analysis

MeasureTheory.integral2_divergence_prod_of_hasFDerivAt

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f g : ℝ × ℝ → E)
  (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ),
  ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) →
    ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) →
      (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt g (g' x) x) →
          MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)
              MeasureTheory.volume →
            ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
              (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
                ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

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 MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le for a version that uses an integral over Icc a b, where a b : ℝ × ℝ, a ≤ b. See also integral2_divergence_prod_of_hasFDerivAt_off_countable for a version that assumes differentiability outside of a countable set.

Defined in

Mathlib.MeasureTheory.Integral.DivergenceTheorem

Cited by

0 results in Mathlib

Foundations

Depth 267 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace