← Mathematical handbook

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

Equations

• Verification.partitionAverage P f i = ∫ (u : ↑unitInterval), f (Verification.partitionEmbed P i u)

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

Equations

• Verification.partitionAverageError P f = ∑ i : Fin n, P.width i * ∫ (u : ↑unitInterval), |Verification.partitionAverage P f i - f (Verification.partitionEmbed P i u)|

theorem Verification.partitionAverage_sub_le {n : ℕ} (P : ProbabilityTheory.Copula.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 Verification.partitionAverageError_nonneg {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (f : ↑unitInterval → ℝ) : 0 ≤ partitionAverageError P f

theorem Verification.partitionAverageError_approx {n : ℕ} (P : ProbabilityTheory.Copula.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 Verification.partitionEmbed_dist_le_width {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) (u v : ↑unitInterval) : dist (partitionEmbed P i u) (partitionEmbed P i v) ≤ P.width i

theorem Verification.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 (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯) i u)) MeasureTheory.volume) : Filter.Tendsto (fun (k : ℕ) => partitionAverageError (ProbabilityTheory.Copula.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.