ae_measure_preimage_mul_right_lt_top_of_ne_zero

English

If ν' s ≠ 0 and s has finite measure, then for a.e. x, the preimage ν' of s under the right-translation is finite and nonzero.

Русский

Если ν'(s) ≠ 0 и μ'(s) не бесконечна, то почти наверняка предобраз ν' по правому сдвигу имеет конечную, непустую меру.

LaTeX

$$$\forall^{\mathrm{ae}} x \partial \mu',\; \nu'( (\cdot * x)^{-1} s) < \infty$ и $\nu'( (\cdot * x)^{-1} s) \neq 0$ при условиях на ν' и s$$

Lean4

@[to_additive]
theorem ae_measure_preimage_mul_right_lt_top_of_ne_zero (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) :
    ∀ᵐ x ∂μ', ν' ((fun y => y * x) ⁻¹' s) < ∞ :=
  by
  refine (ae_measure_preimage_mul_right_lt_top ν' ν' h3s).filter_mono ?_
  refine (absolutelyContinuous_of_isMulLeftInvariant μ' ν' ?_).ae_le
  refine mt ?_ h2s
  intro hν
  rw [hν, Measure.coe_zero, Pi.zero_apply]

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