densityProcess_antitone_kernel_right

English

Concluding the left monotonicity for densityProcess under κ ≤ κ'.

Русский

Завершение левой монотонности densityProcess при κ ≤ κ'.

LaTeX

$$$\text{densityProcess}(\kappa,\nu,n,a,x,s) ≤ \text{densityProcess}(\kappa',\nu,n,a,x,s)$$$

Lean4

theorem densityProcess_antitone_kernel_right {ν' : Kernel α γ} (hνν' : ν ≤ ν') (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (x : γ)
    (s : Set β) : densityProcess κ ν' n a x s ≤ densityProcess κ ν n a x s :=
  by
  unfold densityProcess
  have h_le : κ a (countablePartitionSet n x ×ˢ s) ≤ ν a (countablePartitionSet n x) :=
    meas_countablePartitionSet_le_of_fst_le hκν n a x s
  by_cases h0 : ν a (countablePartitionSet n x) = 0
  · simp [le_antisymm (h_le.trans h0.le) zero_le', h0]
  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νν'

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