← Mathematical handbook

theorem Verification.sklar_map_withDensity_comp {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) {F : X → Y} (hF : Measurable F) {h : Y → ENNReal} (hh : Measurable h) : MeasureTheory.Measure.map F (μ.withDensity fun (x : X) => h (F x)) = (MeasureTheory.Measure.map F μ).withDensity h

theorem Verification.joint_tp2_density_of_copula (J : MeasureTheory.Measure (ℝ × ℝ)) (M : MeasureTheory.Measure ℝ) (m : ℝ → ℝ) (hm : Measurable m) (hn : ∀ (x : ℝ), 0 ≤ m x) (hM : M = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (m x)) (F : ℝ → ↑unitInterval) (hF : Measurable F) (hmono : Monotone F) (hinj : Function.Injective F) (C : ProbabilityTheory.Copula 2) (hprod : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => ![F p.1, F p.2]) (M.prod M) = MeasureTheory.volume) (hC : C.toMeasure = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => ![F p.1, F p.2]) J) (hTP : C.HasMTP2Density) : ∃ (g : ℝ × ℝ → ℝ), Measurable g ∧ (∀ (p : ℝ × ℝ), 0 ≤ g p) ∧ (∀ (a b c d : ℝ), a ≤ b → c ≤ d → g (a, d) * g (b, c) ≤ g (a, c) * g (b, d)) ∧ J = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ENNReal.ofReal (g p)