densityProcess_mono_kernel_left — Mathlib

English

A simplified reflection of densityProcess antitone properties.

Русский

Упрощённое отражение антитонных свойств densityProcess.

LaTeX

$$$\text{densityProcess}_{\text{antitone}}(\cdot)\text{ holds}$$$

Lean4

theorem densityProcess_mono_kernel_left {κ' : Kernel α (γ × β)} (hκκ' : κ ≤ κ') (hκ'ν : fst κ' ≤ ν) (n : ℕ) (a : α)
    (x : γ) (s : Set β) : densityProcess κ ν n a x s ≤ densityProcess κ' ν n a x s :=
  by
  unfold densityProcess
  by_cases h0 : ν a (countablePartitionSet n x) = 0
  · rw [h0, ENNReal.toReal_div, ENNReal.toReal_div]
    simp
  have h_le : κ' a (countablePartitionSet n x ×ˢ s) ≤ ν a (countablePartitionSet n x) :=
    meas_countablePartitionSet_le_of_fst_le hκ'ν n a x s
  gcongr
  · simp only [ne_eq, ENNReal.div_eq_top, h0, and_false, false_or, not_and, not_not]
    exact fun h_top ↦ eq_top_mono h_le h_top
  · apply hκκ'

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