← Mathematical handbook

Finite mixtures of paths with uniform marginals

This constructor allows unequal segment lengths and zero weights. Marginal identities are checked against continuous test functions, and the resulting copula retains an explicit integration formula for its paths.

noncomputable def ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.measure {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (X : ι → ↑unitInterval → Fin 2 → ↑unitInterval) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

Equations

• ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.measure w X = ∑ i : ι, (w i).toNNReal • MeasureTheory.Measure.map (X i) MeasureTheory.volume

instance ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalMeasure {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (X : ι → ↑unitInterval → Fin 2 → ↑unitInterval) : MeasureTheory.IsFiniteMeasure (measure w X)

theorem ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.integral_measure {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (X : ι → ↑unitInterval → Fin 2 → ↑unitInterval) (hX : ∀ (i : ι), Continuous (X i)) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂measure w X = ∑ i : ι, w i * ∫ (u : ↑unitInterval), f (X i u)

theorem ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.map_eval_eq {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (X : ι → ↑unitInterval → Fin 2 → ↑unitInterval) (hX : ∀ (i : ι), Continuous (X i)) (hmarg : ∀ (j : Fin 2) (f : ↑unitInterval → ℝ), Continuous f → ∑ i : ι, w i * ∫ (u : ↑unitInterval), f (X i u j) = ∫ (u : ↑unitInterval), f u) (j : Fin 2) : MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => x j) (measure w X) = MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.copula {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (X : ι → ↑unitInterval → Fin 2 → ↑unitInterval) (hX : ∀ (i : ι), Continuous (X i)) (hmarg : ∀ (j : Fin 2) (f : ↑unitInterval → ℝ), Continuous f → ∑ i : ι, w i * ∫ (u : ↑unitInterval), f (X i u j) = ∫ (u : ↑unitInterval), f u) : Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.copula w hw X hX hmarg = { measure := ⟨ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.measure w X, ⋯⟩, marginal_eq := ⋯ }

theorem ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.integral_copula {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (X : ι → ↑unitInterval → Fin 2 → ↑unitInterval) (hX : ∀ (i : ι), Continuous (X i)) (hmarg : ∀ (j : Fin 2) (f : ↑unitInterval → ℝ), Continuous f → ∑ i : ι, w i * ∫ (u : ↑unitInterval), f (X i u j) = ∫ (u : ↑unitInterval), f u) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(copula w hw X hX hmarg).toMeasure = ∑ i : ι, w i * ∫ (u : ↑unitInterval), f (X i u)

noncomputable def ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.extend (f : ↑unitInterval → ℝ) (x : ℝ) : ℝ

Extend a continuous test function from the unit interval by constant tails.

Equations

• ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.extend f x = f (Set.projIcc 0 1 ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.extend._proof_1 x)

theorem ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.continuous_extend {f : ↑unitInterval → ℝ} (hf : Continuous f) : Continuous (extend f)

@[simp]

theorem ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.extend_coe (f : ↑unitInterval → ℝ) (u : ↑unitInterval) : extend f ↑u = f u

theorem ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.integral_affine (f : ℝ → ℝ) (a b : ℝ) : (b - a) * ∫ (u : ↑unitInterval), f (a + (b - a) * ↑u) = ∫ (u : ℝ) in a..b, f u

Weighted integration of an affine path, including zero-length paths.