rnDeriv_toReal_pos — Mathlib

English

If κ a ≪ η a, then rnDeriv κ η a x has positive real part on a set of positive η a-measure; hence its real part is strictly positive on a set of positive measure almost everywhere.

Русский

Если κa ≪ ηa, то rnDeriv κ η a x имеет положительную вещественную часть на множестве с положительной η a–мерой; следовательно, почти surely её вещественная часть положительна на таком множестве.

LaTeX

$$∗(κ a ≪ η a) → ∀ᵐ x ∂(κ a), (rnDeriv κ η a x).toReal > 0$$

Lean4

theorem rnDeriv_toReal_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) :
    ∀ᵐ x ∂(κ a), 0 < (rnDeriv κ η a x).toReal :=
  by
  filter_upwards [rnDeriv_pos h, h.ae_le (rnDeriv_ne_top κ _)] with x h0 htop
  simp_all only [pos_iff_ne_zero, ne_eq, ENNReal.toReal_pos, not_false_eq_true]

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