SamplingMoments.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Finite-product moments for the sampling argument

All expectations here are finite sums with the actual independent site masses. The variance identities, conditional moments, and absolute-error estimates are proved directly; no moment or independence input is assumed.

theorem OAI.JointDickman.finiteExpectation_add line 23
theorem OAI.JointDickman.finiteExpectation_sub line 27
theorem OAI.JointDickman.finiteExpectation_const_mul line 31
theorem OAI.JointDickman.finiteExpectation_mul_const line 38
theorem OAI.JointDickman.finiteExpectation_const line 42
theorem OAI.JointDickman.finiteExpectation_sum line 46
theorem OAI.JointDickman.finiteExpectation_mono line 51
theorem OAI.JointDickman.finiteExpectation_abs_le_sqrt_sq line 55
theorem OAI.JointDickman.finiteExpectation_centered_sq line 65
theorem OAI.JointDickman.siteProductMass_nonneg line 80
theorem OAI.JointDickman.siteProduct_expectation_prod line 84
Source documentation
The finite sum-product identity supplies independence, with no probabilistic input.
```
theorem siteProduct_expectation_prod (p f : ι → A → ℝ) :
    finiteExpectation (siteProductMass p) (fun x => ∏ i, f i (x i)) =
      ∏ i, finiteExpectation (p i) (f i) := by
…
```
Mentions: OAI.JointDickman.finiteExpectation
theorem OAI.JointDickman.siteProductMass_sum line 91
theorem OAI.JointDickman.siteProduct_expectation_coordinate line 96
theorem OAI.JointDickman.siteProduct_expectation_pair line 110

theorem OAI.JointDickman.siteProduct_centered_sum_sq line 130

Source documentation

Variance of a sum of independent centered single-site functions.

theorem siteProduct_centered_sum_sq (p f : ι → A → ℝ)
    (hpone : ∀ i, ∑ a, p i a = 1) (hf : ∀ i, finiteExpectation (p i) (f i) = 0) :
    finiteExpectation (siteProductMass p) (fun x => (∑ i, f i (x i)) ^ 2) =
      ∑ i, finiteExpectation (p i) (fun a => f i a ^ 2) := by
…

Mentions: OAI.JointDickman.finiteExpectation

theorem OAI.JointDickman.siteProduct_sum_centered_sq line 148
theorem OAI.JointDickman.siteProduct_sum_centered_sq_le line 165
theorem OAI.JointDickman.siteProduct_sum_abs_centered_le line 173
theorem OAI.JointDickman.siteProduct_sum_mean line 182
theorem OAI.JointDickman.siteProduct_sum_sq_le line 191
def OAI.JointDickman.insertSite line 209
Source documentation
Reinsert one fixed site into a configuration on the other sites.
```
def insertSite (k : ι) (a : A) (x : {i : ι // i ≠ k} → A) (i : ι) : A :=
…
```
theorem OAI.JointDickman.insertSite_self line 213
theorem OAI.JointDickman.insertSite_other line 217
theorem OAI.JointDickman.insertSite_restrict line 221
theorem OAI.JointDickman.siteProductMass_insertSite line 227

theorem OAI.JointDickman.siteProduct_disintegrate line 236

Source documentation

Exact finite disintegration at one site; no normalization is needed.

theorem siteProduct_disintegrate (p : ι → A → ℝ) (k : ι) (F : (ι → A) → ℝ) :
    finiteExpectation (siteProductMass p) F =
      finiteExpectation (p k) (fun a =>
        finiteExpectation (siteProductMass (fun i : {i : ι // i ≠ k} => p i))
          (fun x => F (insertSite k a x))) := by
…

Mentions: OAI.JointDickman.finiteExpectation, OAI.JointDickman.insertSite

theorem OAI.JointDickman.siteProduct_expectation_two line 256
def OAI.JointDickman.siteRowSum line 269
Source documentation
A row evaluated on the independent site configuration.
```
noncomputable def siteRowSum (K : ι → ι → A → A → ℝ) (k : ι) (x : ι → A) : ℝ :=
…
```

def OAI.JointDickman.siteRowMean line 273

Source documentation

Its conditional mean after fixing the row site.

noncomputable def siteRowMean (p : ι → A → ℝ) (K : ι → ι → A → A → ℝ)
    (k : ι) (a : A) : ℝ :=
…

def OAI.JointDickman.siteRowSquareMass line 278
Source documentation
Integrated sum of squared row entries, with the row site also averaged.
```
noncomputable def siteRowSquareMass (p : ι → A → ℝ) (K : ι → ι → A → A → ℝ)
    (k : ι) : ℝ :=
…
```
theorem OAI.JointDickman.siteRowSum_insertSite line 284

theorem OAI.JointDickman.siteRowSquareMass_eq_sum_entries line 295

Source documentation

The conditional notation is exactly the integrated squared row used in the manuscript; no stronger pointwise second-moment premise is hidden.

theorem siteRowSquareMass_eq_sum_entries (p : ι → A → ℝ)
    (hpone : ∀ i, ∑ a, p i a = 1) (K : ι → ι → A → A → ℝ)
    (hdiag : ∀ i a, K i i a a = 0) (k : ι) :
    siteRowSquareMass p K k =
      ∑ j, finiteExpectation (siteProductMass p) (fun x => K k j (x k) (x j) ^ 2) := by
…

Mentions: OAI.JointDickman.siteRowSquareMass, OAI.JointDickman.finiteExpectation

theorem OAI.JointDickman.siteRow_centered_sq_le line 313

Source documentation

The integrated conditional variance is bounded by the integrated squared entries. There is no uniform conditional second-moment assumption.

theorem siteRow_centered_sq_le (p : ι → A → ℝ)
    (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (K : ι → ι → A → A → ℝ) (hdiag : ∀ i a, K i i a a = 0) (k : ι) :
    finiteExpectation (siteProductMass p)
      (fun x => (siteRowSum K k x - siteRowMean p K k (x k)) ^ 2) ≤
        siteRowSquareMass p K k := by
…

Mentions: OAI.JointDickman.finiteExpectation, OAI.JointDickman.siteRowSum, OAI.JointDickman.siteRowMean, OAI.JointDickman.siteRowSquareMass

theorem OAI.JointDickman.siteRow_abs_centered_le line 327
theorem OAI.JointDickman.siteRow_abs_mean_le line 337

theorem OAI.JointDickman.siteRow_sq_le line 355

Source documentation

The row second moment follows from its conditional mean and the integrated square mass, even when conditional square masses are large.

theorem siteRow_sq_le (p : ι → A → ℝ)
    (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (K : ι → ι → A → A → ℝ) (hdiag : ∀ i a, K i i a a = 0)
    (k : ι) (C : ℝ) (hmean : ∀ a, |siteRowMean p K k a| ≤ C) :
    finiteExpectation (siteProductMass p) (fun x => siteRowSum K k x ^ 2) ≤
      C ^ 2 + siteRowSquareMass p K k := by
…

Mentions: OAI.JointDickman.siteRowMean, OAI.JointDickman.finiteExpectation, OAI.JointDickman.siteRowSum, OAI.JointDickman.siteRowSquareMass

theorem OAI.JointDickman.siteRow_total_abs_mean_le line 384

Source documentation

Sum of the conditional column-mean comparisons, in the normalization before dividing by the number of sites.

theorem siteRow_total_abs_mean_le (p : ι → A → ℝ)
    (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (K : ι → ι → A → A → ℝ) (hdiag : ∀ i a, K i i a a = 0) :
    finiteExpectation (siteProductMass p) (fun x => ∑ k, |siteRowSum K k x|) ≤
      (∑ k, finiteExpectation (p k) (fun a => |siteRowMean p K k a|)) +
        ∑ k, Real.sqrt (siteRowSquareMass p K k) := by
…

Mentions: OAI.JointDickman.finiteExpectation, OAI.JointDickman.siteRowSum, OAI.JointDickman.siteRowMean, OAI.JointDickman.siteRowSquareMass

theorem OAI.JointDickman.siteRow_multiply_test_mean line 393

theorem OAI.JointDickman.siteRow_total_abs_of_tests line 410

Source documentation

Fixed single-site tests suffice to control the mean after the sampled columns have been fixed. The optimizing test is the sign of the conditional column mean, not a function of the remaining full configuration.

theorem siteRow_total_abs_of_tests (p : ι → A → ℝ)
    (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (K : ι → ι → A → A → ℝ) (hdiag : ∀ i a, K i i a a = 0) (C : ℝ)
    (htest : ∀ h : ι → A → ℝ, (∀ i a, |h i a| ≤ 1) →
      finiteExpectation (siteProductMass p) (fun x => ∑ k, siteRowSum K k x * h k (x k)) ≤ C) :
    finiteExpectation (siteProductMass p) (fun x => ∑ k, |siteRowSum K k x|) ≤
      C + ∑ k, Real.sqrt (siteRowSquareMass p K k) := by
…

Mentions: OAI.JointDickman.finiteExpectation, OAI.JointDickman.siteRowSum, OAI.JointDickman.siteRowSquareMass