iInf_rat_gt_eq — Mathlib

English

For a fixed a, almost every t satisfies ⨅ r>I o f(a,t) r = f(a,t) q for every q ∈ ℚ.

Русский

Для фиксированного a почти верно, что ∀ q ∈ ℚ: инфимf f(a,t) r по r>I q равен f(a,t) q.

LaTeX

$$$\forall a,\; \text{ae}_{t\sim ν(a)}(\forall q\in\mathbb{Q}, \; \iInf_{r>I q} f(a,t) r = f(a,t) q).$$$

Lean4

theorem iInf_rat_gt_eq (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) :
    ∀ᵐ t ∂(ν a), ∀ q : ℚ, ⨅ r : Ioi q, f (a, t) r = f (a, t) q :=
  by
  rw [ae_all_iff]
  refine fun q ↦ ae_eq_of_forall_setIntegral_eq_of_sigmaFinite (μ := ν a) ?_ ?_ ?_
  · exact fun _ _ _ ↦ (hf.integrable_iInf_rat_gt _ _).integrableOn
  · exact fun _ _ _ ↦ (hf.integrable a _).integrableOn
  · intro s hs _
    rw [hf.setIntegral _ hs, hf.setIntegral_iInf_rat_gt _ _ hs]

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