integral_divergence_of_hasFDerivAt_off_countable_of_equiv

English

Divergence theorem for a plane rectangle: the integral of the divergence over the rectangle equals the sum of boundary contributions on the four sides.

Русский

Теорема дивергенции для плоского прямоугольника: интеграл дивергенции по прямоугольнику равен сумме вкладов по границе четырёх сторон.

LaTeX

$$$\\int_{[a,b]} \\nabla\\cdot F = \\text{boundary contributions on four sides}$$$

Lean4

/-- An auxiliary lemma that is used to specialize the general divergence theorem to spaces that do
not have the form `Fin n → ℝ`. -/
theorem integral_divergence_of_hasFDerivAt_off_countable_of_equiv {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    [Preorder F] [MeasureSpace F] [BorelSpace F] (eL : F ≃L[ℝ] ℝⁿ⁺¹) (he_ord : ∀ x y, eL x ≤ eL y ↔ x ≤ y)
    (he_vol : MeasurePreserving eL volume volume) (f : Fin (n + 1) → F → E) (f' : Fin (n + 1) → F → F →L[ℝ] E)
    (s : Set F) (hs : s.Countable) (a b : F) (hle : a ≤ b) (Hc : ∀ i, ContinuousOn (f i) (Icc a b))
    (Hd : ∀ x ∈ interior (Icc a b) \ s, ∀ (i), HasFDerivAt (f i) (f' i x) x) (DF : F → E)
    (hDF : ∀ x, DF x = ∑ i, f' i x (eL.symm <| e i)) (Hi : IntegrableOn DF (Icc a b)) :
    ∫ x in Icc a b, DF x =
      ∑ i : Fin (n + 1),
        ((∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm <| i.insertNth (eL b i) x)) -
          ∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm <| i.insertNth (eL a i) x)) :=
  have he_emb : MeasurableEmbedding eL := eL.toHomeomorph.measurableEmbedding
  have hIcc : eL ⁻¹' Icc (eL a) (eL b) = Icc a b := by ext1 x; simp only [Set.mem_preimage, Set.mem_Icc, he_ord]
  have hIcc' : Icc (eL a) (eL b) = eL.symm ⁻¹' Icc a b := by rw [← hIcc, eL.symm_preimage_preimage]
  calc
    ∫ x in Icc a b, DF x = ∫ x in Icc a b, ∑ i, f' i x (eL.symm <| e i) := by simp only [hDF]
    _ = ∫ x in Icc (eL a) (eL b), ∑ i, f' i (eL.symm x) (eL.symm <| e i) :=
      by
      rw [← he_vol.setIntegral_preimage_emb he_emb]
      simp only [hIcc, eL.symm_apply_apply]
    _ =
        ∑ i : Fin (n + 1),
          ((∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm <| i.insertNth (eL b i) x)) -
            ∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm <| i.insertNth (eL a i) x)) :=
      by
      refine
        integral_divergence_of_hasFDerivAt_off_countable' (eL a) (eL b) ((he_ord _ _).2 hle)
          (fun i x => f i (eL.symm x)) (fun i x => f' i (eL.symm x) ∘L (eL.symm : ℝⁿ⁺¹ →L[ℝ] F)) (eL.symm ⁻¹' s)
          (hs.preimage eL.symm.injective) ?_ ?_ ?_
      · exact fun i => (Hc i).comp eL.symm.continuousOn hIcc'.subset
      · refine fun x hx i => (Hd (eL.symm x) ⟨?_, hx.2⟩ i).comp x eL.symm.hasFDerivAt
        rw [← hIcc]
        refine preimage_interior_subset_interior_preimage eL.continuous ?_
        simpa only [Set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc, interior_pi_set (@finite_univ (Fin _) _),
          interior_Icc] using hx.1
      · rw [← he_vol.integrableOn_comp_preimage he_emb, hIcc]
        simp [← hDF, Function.comp_def, Hi]

Похожие утверждения