integral_congr_codiscreteWithin — Mathlib

English

Integrals are invariant under codiscreteWithin perturbations on the restricted interval.

Русский

Интегралы не изменяются при неконецентрированных возмущениях на ограниченном интервале.

LaTeX

$$$ ∫_{I} f \\, dμ = ∫_{I} g \\, dμ \\text{ if } f =^{\\text{ae}}_{codiscreteWithin(I)} g $$$

Lean4

/-- Integrals are invariant when functions change along discrete sets. -/
theorem integral_congr_codiscreteWithin {a b : ℝ} {f₁ f₂ : ℝ → ℝ} (hf : f₁ =ᶠ[codiscreteWithin (Ι a b)] f₂) :
    ∫ (x : ℝ) in a..b, f₁ x = ∫ (x : ℝ) in a..b, f₂ x :=
  integral_congr_ae_restrict (ae_restrict_le_codiscreteWithin measurableSet_uIoc hf)

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