Theorems · Theorem · real analysis

BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [CompleteSpace E]
  (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {f : (Fin (n + 1) → ℝ) → E} {f' : (Fin (n + 1) → ℝ) →L[ℝ] E},
  ContinuousOn f (BoxIntegral.Box.Icc I) →
    ∀ {x : Fin (n + 1) → ℝ},
      x ∈ BoxIntegral.Box.Icc I →
        ∀ {a : E} {ε : ℝ},
          0 < ε →
            (∀ y ∈ BoxIntegral.Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖) →
              ∀ {c : NNReal},
                I.distortion ≤ c →
                  ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
                        (BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.upper i))
                            BoxIntegral.BoxAdditiveMap.volume -
                          BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.lower i))
                            BoxIntegral.BoxAdditiveMap.volume)‖ ≤
                    2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)

Auxiliary lemma for the divergence theorem.

Defined in

Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace