Fin

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Efron–Stein on finite products indexed by Fin n

Elementary induction on the number of coordinates, splitting off coordinate 0 via MeasurableEquiv.piFinSuccAbove.

theorem HCPolySupport.update_symm_zero {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → MeasurableSpace (α i)] (p : α 0 × ((j : Fin n) → α (Fin.succAbove 0 j))) (y : α 0) : Function.update ((MeasurableEquiv.piFinSuccAbove α 0).symm p) 0 y = (MeasurableEquiv.piFinSuccAbove α 0).symm (y, p.2)

Updating coordinate 0 of e.symm p to y re-inserts y in the first slot.

theorem HCPolySupport.update_symm_succ {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → MeasurableSpace (α i)] (p : α 0 × ((j : Fin n) → α (Fin.succAbove 0 j))) (j : Fin n) (y : α (Fin.succAbove 0 j)) : Function.update ((MeasurableEquiv.piFinSuccAbove α 0).symm p) (Fin.succAbove 0 j) y = (MeasurableEquiv.piFinSuccAbove α 0).symm (p.1, Function.update p.2 j y)

Updating coordinate succAbove 0 j of e.symm p corresponds to updating tail slot j.

theorem HCPolySupport.term_zero_eq {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → MeasurableSpace (α i)] (μ : (i : Fin (n + 1)) → MeasureTheory.Measure (α i)) [∀ (i : Fin (n + 1)), MeasureTheory.IsProbabilityMeasure (μ i)] {F : ((i : Fin (n + 1)) → α i) → ℝ} (hF : Measurable F) {M : ℝ} (hM : ∀ (x : (i : Fin (n + 1)) → α i), |F x| ≤ M) : (∫ (t : (i : Fin n) → α (Fin.succAbove 0 i)), ProbabilityTheory.variance (fun (a : α 0) => F ((MeasurableEquiv.piFinSuccAbove α 0).symm (a, t))) (μ 0) ∂MeasureTheory.Measure.pi fun (j : Fin n) => μ (Fin.succAbove 0 j)) = 1 / 2 * ∫ (x : (i : Fin (n + 1)) → α i), ∫ (y : α 0), (F (Function.update x 0 y) - F x) ^ 2 ∂μ 0 ∂MeasureTheory.Measure.pi μ

The coordinate-0 conditional-variance integral equals half the coordinate-0 resampling energy.

theorem HCPolySupport.term_succ_le {n : ℕ} {α : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → MeasurableSpace (α i)] (μ : (i : Fin (n + 1)) → MeasureTheory.Measure (α i)) [∀ (i : Fin (n + 1)), MeasureTheory.IsProbabilityMeasure (μ i)] {F : ((i : Fin (n + 1)) → α i) → ℝ} (hF : Measurable F) {M : ℝ} (hM : ∀ (x : (i : Fin (n + 1)) → α i), |F x| ≤ M) (j : Fin n) : (∫ (t : (i : Fin n) → α (Fin.succAbove 0 i)), ∫ (w : α (Fin.succAbove 0 j)), (∫ (a : α 0), F ((MeasurableEquiv.piFinSuccAbove α 0).symm (a, Function.update t j w)) ∂μ 0 - ∫ (a : α 0), F ((MeasurableEquiv.piFinSuccAbove α 0).symm (a, t)) ∂μ 0) ^ 2 ∂μ (Fin.succAbove 0 j) ∂MeasureTheory.Measure.pi fun (k : Fin n) => μ (Fin.succAbove 0 k)) ≤ ∫ (x : (i : Fin (n + 1)) → α i), ∫ (y : α (Fin.succAbove 0 j)), (F (Function.update x (Fin.succAbove 0 j) y) - F x) ^ 2 ∂μ (Fin.succAbove 0 j) ∂MeasureTheory.Measure.pi μ

The tail (coordinate succAbove 0 j) contribution: the resampling energy of the conditional mean g' is bounded by the full resampling energy of F.

theorem HCPolySupport.efronStein_fin (m : ℕ) {β : Fin m → Type u_2} [(i : Fin m) → MeasurableSpace (β i)] (μ : (i : Fin m) → MeasureTheory.Measure (β i)) [∀ (i : Fin m), MeasureTheory.IsProbabilityMeasure (μ i)] {F : ((i : Fin m) → β i) → ℝ} (_hF : Measurable F) {M : ℝ} (_hM : ∀ (x : (i : Fin m) → β i), |F x| ≤ M) : ProbabilityTheory.variance F (MeasureTheory.Measure.pi μ) ≤ 1 / 2 * ∑ i : Fin m, ∫ (x : (i : Fin m) → β i), ∫ (y : β i), (F (Function.update x i y) - F x) ^ 2 ∂μ i ∂MeasureTheory.Measure.pi μ

Efron–Stein inequality for bounded measurable observables on a finite product Fin m (proved by induction on m).

theorem HCPolySupport.efronStein_pi {ι : Type u_2} [Fintype ι] [DecidableEq ι] {Ω : ι → Type u_3} [(i : ι) → MeasurableSpace (Ω i)] (μ : (i : ι) → MeasureTheory.Measure (Ω i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {F : ((i : ι) → Ω i) → ℝ} (hF : Measurable F) {M : ℝ} (hM : ∀ (x : (i : ι) → Ω i), |F x| ≤ M) : ProbabilityTheory.variance F (MeasureTheory.Measure.pi μ) ≤ 1 / 2 * ∑ i : ι, ∫ (x : (i : ι) → Ω i), ∫ (y : Ω i), (F (Function.update x i y) - F x) ^ 2 ∂μ i ∂MeasureTheory.Measure.pi μ

Efron–Stein inequality for bounded measurable observables on an arbitrary finite product probability space.