lintegral_eq_zero_of_isMulLeftInvariant

English

For a nonzero regular left-invariant measure μ and a continuous nonnegative function f: G → ℝ≥0∞, the integral ∫ f dμ is zero if and only if f is identically zero.

Русский

Для не нулевой регулярной левой инвариантной меры μ и непрерывной неотрицательной функции f: G → ℝ≥0∞ выполнено: интеграл нулю тогда, когда f ≡ 0.

LaTeX

$$$$ \\int_G f(x) \\, d\\mu(x) = 0 \\iff f = 0. $$$$

Lean4

/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function
  `f` is 0 iff `f` is 0. -/
@[to_additive /-- For nonzero regular left invariant measures, the integral of a continuous nonnegative
          function `f` is 0 iff `f` is 0. -/
    ]
theorem lintegral_eq_zero_of_isMulLeftInvariant [Regular μ] [NeZero μ] {f : G → ℝ≥0∞} (hf : Continuous f) :
    ∫⁻ x, f x ∂μ = 0 ↔ f = 0 := by rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]

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