English
For each a, q ∈ ℚ, the function t ↦ ⨅ r>I q f(a,t) r is integrable with respect to (ν a).
Русский
Для каждого a и q функция t ↦ ⨅_{r>I q} f(a,t) r интегрируема по ν(a).
LaTeX
$$$\forall a\in\alpha,\; \forall q\in\mathbb{Q},\; \text{Integrable}\bigl(t\mapsto \inf_{r>I q} f(a,t) r\bigr)\ bigl(ν a\bigr).$$$
Lean4
theorem integrable_iInf_rat_gt (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel ν] (a : α) (q : ℚ) :
Integrable (fun t ↦ ⨅ r : Ioi q, f (a, t) r) (ν a) :=
by
rw [← memLp_one_iff_integrable]
refine ⟨(Measurable.iInf fun i ↦ hf.measurable_right a _).aestronglyMeasurable, ?_⟩
refine (?_ : _ ≤ (ν a univ : ℝ≥0∞)).trans_lt (measure_lt_top _ _)
refine (eLpNorm_le_of_ae_bound (C := 1) ?_).trans (by simp)
filter_upwards [hf.bddBelow_range a, hf.nonneg a, hf.le_one a] with t hbdd_below h_nonneg h_le_one
rw [Real.norm_eq_abs, abs_of_nonneg]
· refine ciInf_le_of_le ?_ ?_ ?_
· exact hbdd_below _
· exact ⟨q + 1, by simp⟩
· exact h_le_one _
· exact le_ciInf fun r ↦ h_nonneg _
