English
For hf and finite κ,ν, and measurable A, ∫_A t iInf_{r>I q} f(a,t) r d(ν a) equals (κ a).real(A × Iic q).
Русский
Для hf и конечных κ,ν, при измеримом A, интеграл по A от t с iInf_{r>I q} f(a,t) r по ν(a) равен мере κ(a) на A×Iic(q).
LaTeX
$$$\int_{t\in A} \iinf_{r>I q} f(a,t) r \, d(ν a)(t) = (κ a).real\bigl(A × I_i c q\bigr).$$$
Lean4
theorem setIntegral_iInf_rat_gt (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) (q : ℚ)
{A : Set β} (hA : MeasurableSet A) : ∫ t in A, ⨅ r : Ioi q, f (a, t) r ∂(ν a) = (κ a).real (A ×ˢ Iic (q : ℝ)) :=
by
refine le_antisymm ?_ ?_
· have h : ∀ r : Ioi q, ∫ t in A, ⨅ r' : Ioi q, f (a, t) r' ∂(ν a) ≤ (κ a).real (A ×ˢ Iic (r : ℝ)) :=
by
intro r
rw [← hf.setIntegral a hA]
refine setIntegral_mono_ae ?_ ?_ ?_
· exact (hf.integrable_iInf_rat_gt _ _).integrableOn
· exact (hf.integrable _ _).integrableOn
· filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r
calc
∫ t in A, ⨅ r : Ioi q, f (a, t) r ∂(ν a) ≤ ⨅ r : Ioi q, (κ a).real (A ×ˢ Iic (r : ℝ)) := le_ciInf h
_ = (κ a).real (A ×ˢ Iic (q : ℝ)) :=
by
rw [measureReal_def, ← Measure.iInf_rat_gt_prod_Iic hA q]
exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm
· rw [← hf.setIntegral a hA]
refine setIntegral_mono_ae ?_ ?_ ?_
· exact (hf.integrable _ _).integrableOn
· exact (hf.integrable_iInf_rat_gt _ _).integrableOn
· filter_upwards [hf.mono a] with c h_mono using le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))
