absolutelyContinuous_compProd_iff'

English

If μ and ν are finite (SFinite) and κ a ≠ 0 for all a, then μ ⊗ κ ≪ ν ⊗ η if and only if μ ≪ ν and ∀ᵐ a ∂ μ, κ a ≪ η a.

Русский

Если μ и ν конечны (SFinite) и для всех a κ(a) ≠ 0, тогда μ ⊗ κ ⪯ ν ⊗ η тогда и только тогда μ ⪯ ν и ∀ᵐ a ∂ μ, κ(a) ≪ η(a).

LaTeX

$$$(μ \\otimes κ) \\ll (ν \\otimes η) \\iff (μ \\ll ν) \\land (\\forall^{\\text{ae}} a\\partial μ,\\ κ(a) \\ll η(a)).$$$

Lean4

theorem absolutelyContinuous_compProd_iff' [SFinite μ] [SFinite ν] [∀ a, NeZero (κ a)] :
    μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a :=
  ⟨fun h ↦ ⟨absolutelyContinuous_of_compProd h, h.kernel_of_compProd⟩, fun h ↦ h.1.compProd h.2⟩

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