MixedDifference.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Exact singleton centering

The product sampling law is kept fixed. Forcing a coordinate overwrites that coordinate of the same sample, rather than drawing fresh coordinates at different sites. This is the algebraic part of q:mixed-difference.

def OAI.TwoPointCorrelations.forceCoordinates line 19
lemma OAI.TwoPointCorrelations.forceCoordinates_apply line 22
def OAI.TwoPointCorrelations.mixedDifference line 25
lemma OAI.TwoPointCorrelations.FiniteLaw.average_const_mul line 31
lemma OAI.TwoPointCorrelations.FiniteLaw.abs_average_le line 39
lemma OAI.TwoPointCorrelations.FiniteLaw.average_singleton_pin line 47
lemma OAI.TwoPointCorrelations.FiniteLaw.singleton_centering line 51
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_pin line 67
lemma OAI.TwoPointCorrelations.FiniteLaw.force_join line 80
theorem OAI.TwoPointCorrelations.FiniteLaw.independent_forcing line 89
Source documentation
Forcing a selected set has precisely the product mass of its forced atoms, even when the observable depends on every other coordinate.
```
theorem independent_forcing (μ : ι → FiniteLaw A) (S : Finset ι)
    (a : ι → A) (F : (ι → A) → ℝ) :
    (independent μ).average (fun x =>
      (∏ i ∈ S, if x i = a i then (1 : ℝ) else 0) * F x) =
      (∏ i ∈ S, (μ i).weight (a i)) *
        (independent μ).average (fun x => F (forceCoordinates S a x)) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average, OAI.TwoPointCorrelations.forceCoordinates
theorem OAI.TwoPointCorrelations.FiniteLaw.exact_mixed_centering line 120
Source documentation
Centering every singleton is exactly the alternating sum over forcing subsets, before any absolute value is taken.
```
theorem exact_mixed_centering (μ : ι → FiniteLaw A) (a : ι → A)
    (F : (ι → A) → ℝ) :
    (independent μ).average (fun x =>
      (∏ i, ((if x i = a i then (1 : ℝ) else 0) - (μ i).weight (a i))) * F x) =
      (∏ i, (μ i).weight (a i)) * (independent μ).average (mixedDifference a F) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average, OAI.TwoPointCorrelations.mixedDifference
theorem OAI.TwoPointCorrelations.FiniteLaw.mixed_centering_bound line 163

theorem OAI.TwoPointCorrelations.FiniteLaw.exact_designated_centering line 177

Source documentation

A designated trace term: lit nonsingletons are pinned and singleton coordinates are centered. The scalar includes all unlit signs and every factor independent of these residue draws.

theorem exact_designated_centering {κ C : Type*} [Fintype κ] [DecidableEq κ]
    [Fintype C] [DecidableEq C]
    (μ : ι → FiniteLaw A) (ν : κ → FiniteLaw C) (a : ι → A) (b : κ → C)
    (s : ℝ) (F : (ι → A) → (κ → C) → ℝ) :
    (independent μ).average (fun x => (independent ν).average (fun y =>
      s * (∏ i, ((if x i = a i then (1 : ℝ) else 0) - (μ i).weight (a i))) *
        (∏ j, if y j = b j then (1 : ℝ) else 0) * F x y)) =
      s * (∏ j, (ν j).weight (b j)) * (∏ i, (μ i).weight (a i)) *
        (independent μ).average (mixedDifference a (fun x => F x b)) := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average, OAI.TwoPointCorrelations.mixedDifference

theorem OAI.TwoPointCorrelations.abs_mixedDifference_le line 208
theorem OAI.TwoPointCorrelations.exists_forced_value_ne_zero line 224
Source documentation
A nonzero alternating difference has a nonzero hybrid term.
```
theorem exists_forced_value_ne_zero (a : ι → A) (F : (ι → A) → ℝ) (x : ι → A)
    (h : mixedDifference a F x ≠ 0) :
    ∃ S : Finset ι, F (forceCoordinates S a x) ≠ 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.mixedDifference, OAI.TwoPointCorrelations.forceCoordinates