← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionAverage {n : ℕ} (P : IntervalPartition n) (f : ↑unitInterval → ℝ) (i : Fin n) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionAverage P f i = ∫ (u : ↑unitInterval), f (ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed P i u)

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionAverageError {n : ℕ} (P : IntervalPartition n) (f : ↑unitInterval → ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionAverage_sub_le {n : ℕ} (P : IntervalPartition n) (f g : ↑unitInterval → ℝ) (i : Fin n) (hf : MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (partitionEmbed P i u)) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (u : ↑unitInterval) => g (partitionEmbed P i u)) MeasureTheory.volume) : |partitionAverage P f i - partitionAverage P g i| ≤ ∫ (u : ↑unitInterval), |f (partitionEmbed P i u) - g (partitionEmbed P i u)|

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionAverageError_nonneg {n : ℕ} (P : IntervalPartition n) (f : ↑unitInterval → ℝ) : 0 ≤ partitionAverageError P f

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionAverageError_approx {n : ℕ} (P : IntervalPartition n) (f g : ↑unitInterval → ℝ) (hf : Measurable f) (hg : Measurable g) (hfi : ∀ (i : Fin n), MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (partitionEmbed P i u)) MeasureTheory.volume) (hgi : ∀ (i : Fin n), MeasureTheory.Integrable (fun (u : ↑unitInterval) => g (partitionEmbed P i u)) MeasureTheory.volume) (δ : ℝ) (hδ : ∀ (i : Fin n) (u v : ↑unitInterval), |g (partitionEmbed P i u) - g (partitionEmbed P i v)| ≤ δ) : partitionAverageError P f ≤ (2 * ∫ (u : ↑unitInterval), |f u - g u|) + δ

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionEmbed_dist_le_width {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u v : ↑unitInterval) : dist (partitionEmbed P i u) (partitionEmbed P i v) ≤ P.width i

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionAverageError_tendsto (f : ↑unitInterval → ℝ) (hf : Measurable f) (hi : MeasureTheory.Integrable f MeasureTheory.volume) (hfi : ∀ (k : ℕ) (i : Fin (k + 1)), MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (partitionEmbed (IntervalPartition.uniform (k + 1) ⋯) i u)) MeasureTheory.volume) : Filter.Tendsto (fun (k : ℕ) => partitionAverageError (IntervalPartition.uniform (k + 1) ⋯) f) Filter.atTop (nhds 0)

Cell averaging on uniform grids converges in L1 for every measurable integrable function whose restrictions through the affine cell maps are integrable.