mutuallySingularSet — Mathlib

English

Define the set of points in α × γ where rnDerivAux κ (κ+η) a x is at least 1; this characterizes where κ and η are mutually singular relative to κ+η.

Русский

Определим множество точек в α × γ, для которых rnDerivAux κ (κ+η) a x не меньше 1; оно описывает взаимную сингулярность κ и η относительно κ+η.

LaTeX

$$$\text{mutuallySingularSet}(\kappa, \eta) = \{ (a, x) \in \alpha \times \gamma : 1 \le \mathrm{rnDerivAux}(\kappa, \kappa + \eta)(a, x) \}$$$

Lean4

/-- A set of points in `α × γ` related to the absolute continuity / mutual singularity of
`κ` and `η`. -/
def mutuallySingularSet (κ η : Kernel α γ) : Set (α × γ) :=
  {p | 1 ≤ rnDerivAux κ (κ + η) p.1 p.2}

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