intervalAverage_congr_codiscreteWithin

English

If two functions agree on a codiscrete portion of the interval a..b, then their interval averages are equal.

Русский

Если две функции совпадают на кодискретной части интервала a..b, то их средние по интервалу совпадают.

LaTeX

$$$$\langle f_1 \rangle_{[a,b]} = \langle f_2 \rangle_{[a,b]}\quad\text{whenever } f_1 = f_2 \text{ on } Ι[a,b].$$$$

Lean4

/-- Interval averages are invariant when functions change along discrete sets. -/
theorem intervalAverage_congr_codiscreteWithin {a b : ℝ} {f₁ f₂ : ℝ → ℝ}
    (hf : f₁ =ᶠ[Filter.codiscreteWithin (Ι a b)] f₂) : ⨍ (x : ℝ) in a..b, f₁ x = ⨍ (x : ℝ) in a..b, f₂ x := by
  rw [interval_average_eq, intervalIntegral.integral_congr_codiscreteWithin hf, ← interval_average_eq]

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