nonneg — Mathlib

English

For hf, for a fixed a, there is an almost-everywhere property that for all rational q, f(a,c) q ≥ 0 for a.e. c with respect to ν(a).

Русский

Для hf для фиксированного a выполняется почти всюду: для всех q ∈ ℚ, f(a,c) q ≥ 0 для а.е. c по ν(a).

LaTeX

$$$\forall a,\; \text{ae}_{c\sim ν(a)}(\forall q\in\mathbb{Q}, f(a,c) q \ge 0).$$$

Lean4

theorem nonneg (hf : IsRatCondKernelCDFAux f κ ν) (a : α) : ∀ᵐ c ∂(ν a), ∀ q, 0 ≤ f (a, c) q :=
  ae_all_iff.mpr <| hf.nonneg' a

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