PartialCentering.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact singleton centering on selected coordinates of the complete residue sample.

def OAI.TwoPointCorrelations.selectedMixedDifference line 13
lemma OAI.TwoPointCorrelations.selectedMixedDifference_join line 20
lemma OAI.TwoPointCorrelations.selectedMixedDifference_bound line 27
theorem OAI.TwoPointCorrelations.FiniteLaw.exact_selected_centering line 39
Source documentation
The unselected coordinates remain part of the original sample, and are simply held fixed while applying the exact centering identity.
```
theorem exact_selected_centering (μ : ι → FiniteLaw A) (S : Finset ι)
    (a : ι → A) (F : (ι → A) → ℝ) :
    (independent μ).average (fun x =>
      (∏ i ∈ S, ((if x i = a i then (1 : ℝ) else 0) - (μ i).weight (a i))) * F x) =
      (∏ i ∈ S, (μ i).weight (a i)) *
        (independent μ).average (selectedMixedDifference S a F) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average, OAI.TwoPointCorrelations.selectedMixedDifference

theorem OAI.TwoPointCorrelations.FiniteLaw.exact_selected_designation line 70

Source documentation

Nonsingletons with at least one lit occurrence are forced once. The singleton coordinates are then centered on the same sample.

theorem exact_selected_designation (μ : ι → FiniteLaw A) (S T : Finset ι)
    (hST : Disjoint S T) (a b : ι → A) (F : (ι → A) → ℝ) :
    (independent μ).average (fun x =>
      (∏ i ∈ T, if x i = b i then (1 : ℝ) else 0) *
      ((∏ i ∈ S, ((if x i = a i then (1 : ℝ) else 0) - (μ i).weight (a i))) * F x)) =
      (∏ i ∈ T, (μ i).weight (b i)) * (∏ i ∈ S, (μ i).weight (a i)) *
        (independent μ).average
          (selectedMixedDifference S a (fun x => F (forceCoordinates T b x))) := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average, OAI.TwoPointCorrelations.selectedMixedDifference, OAI.TwoPointCorrelations.forceCoordinates

theorem OAI.TwoPointCorrelations.FiniteLaw.selected_designation_bound line 93

Source documentation

The absolute value is taken only after singleton integration, retaining the full cancellation caused by the mixed difference.

theorem selected_designation_bound (μ : ι → FiniteLaw A) (S T : Finset ι)
    (hST : Disjoint S T) (a b : ι → A) (F : (ι → A) → ℝ) :
    |(independent μ).average (fun x =>
      (∏ i ∈ T, if x i = b i then (1 : ℝ) else 0) *
      ((∏ i ∈ S, ((if x i = a i then (1 : ℝ) else 0) - (μ i).weight (a i))) * F x))| ≤
      (∏ i ∈ T, (μ i).weight (b i)) * (∏ i ∈ S, (μ i).weight (a i)) *
        (independent μ).average (fun x =>
          |selectedMixedDifference S a (fun x => F (forceCoordinates T b x)) x|) := by
…