mutuallySingularSetSlice — Mathlib

English

For a fixed a, the set of γ-points where 1 ≤ rnDerivAux κ (κ+η) a x defines a slice of γ dependent on a.

Русский

Для фиксированного a множество точек γ, где 1 ≤ rnDerivAux κ (κ+η) a x, образует срез γ в зависимости от a.

LaTeX

$$$\text{mutuallySingularSetSlice}(\kappa, \eta)(a) = \{ x \in \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 `η`. That is,
* `withDensity η (rnDeriv κ η) a (mutuallySingularSetSlice κ η a) = 0`,
* `singularPart κ η a (mutuallySingularSetSlice κ η a)ᶜ = 0`.
-/
def mutuallySingularSetSlice (κ η : Kernel α γ) (a : α) : Set γ :=
  {x | 1 ≤ rnDerivAux κ (κ + η) a x}

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