← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.integrable_bounded_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : Measurable f) (hb : ∀ (x : Ω), ‖f x‖ ≤ 1) : MeasureTheory.Integrable f μ

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.norm_integral_bounded_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ℝ} (hb : ∀ (x : Ω), ‖f x‖ ≤ 1) : ‖∫ (x : Ω), f x ∂μ‖ ≤ 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_integral_bounded_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : ℕ → Ω → ℝ} {g : Ω → ℝ} (hf : ∀ (n : ℕ), Measurable (f n)) (hb : ∀ (n : ℕ) (x : Ω), ‖f n x‖ ≤ 1) (ht : ∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Ω), f n x ∂μ) Filter.atTop (nhds (∫ (x : Ω), g x ∂μ))