CoordinateSampling.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Factor the full independent law into controls, pivots and outside coordinates.

lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_equiv line 18
Source documentation
A bijection of coordinate names preserves a constant independent law.
```
lemma independent_average_equiv (e : ι ≃ κ) (μ : FiniteLaw A)
    (f : (κ → A) → ℝ) :
    (independent (fun _ : κ => μ)).average f =
      (independent (fun _ : ι => μ)).average (fun x => f (fun k => x (e.symm k))) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_sum line 36
Source documentation
Independence on a sum of coordinate types is the product of the two independent laws.
```
lemma independent_average_sum (μ : FiniteLaw A) (f : (ι ⊕ κ → A) → ℝ) :
    (independent (fun _ : ι ⊕ κ => μ)).average f =
      (independent (fun _ : ι => μ)).average (fun x =>
        (independent (fun _ : κ => μ)).average (fun y => f (Sum.elim x y))) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average
abbrev OAI.TwoPointCorrelations.OutsideIndex line 59
def OAI.TwoPointCorrelations.coordinateIndex line 61
lemma OAI.TwoPointCorrelations.coordinateIndex_bijective line 65
def OAI.TwoPointCorrelations.coordinateEquiv line 100
def OAI.TwoPointCorrelations.coordinateAssignment line 106
lemma OAI.TwoPointCorrelations.coordinateAssignment_index line 113

theorem OAI.TwoPointCorrelations.independent_average_three line 125

Source documentation

Full product-law factorization, with the outside coordinates averaged last in the proof and moved to the outermost expectation in the result.

theorem independent_average_three [Fintype A]
    (control pivot : ρ → α) (hc : Function.Injective control) (hp : Function.Injective pivot)
    (hdisjoint : ∀ i j, pivot i ≠ control j) (μ : FiniteLaw A) (f : (α → A) → ℝ) :
    (FiniteLaw.independent (fun _ : α => μ)).average f =
      (FiniteLaw.independent (fun _ : OutsideIndex control pivot => μ)).average (fun base =>
        (FiniteLaw.independent (fun _ : ρ => μ)).average (fun c =>
          (FiniteLaw.independent (fun _ : ρ => μ)).average (fun y =>
            f (coordinateAssignment control pivot hc hp hdisjoint base c y)))) := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.OutsideIndex, OAI.TwoPointCorrelations.coordinateAssignment

lemma OAI.TwoPointCorrelations.coordinateAssignment_integer line 154

Source documentation

Evaluation of the joined samples is the exact integer assignment used in the row-splitting theorem.

lemma coordinateAssignment_integer (control pivot : ρ → α)
    (hc : Function.Injective control) (hp : Function.Injective pivot)
    (hdisjoint : ∀ i j, pivot i ≠ control j) (value : A → ℤ)
    (base : OutsideIndex control pivot → A) (c y : ρ → A) :
    (fun z => value (coordinateAssignment control pivot hc hp hdisjoint base c y z)) =
      splitAssignment control pivot
        (fun z => if hz : z ∈ outsideCoordinates control pivot then value (base ⟨z, hz⟩) else 0)
        (fun i => value (c i)) (fun i => value (y i)) := by
…

Mentions: OAI.TwoPointCorrelations.OutsideIndex, OAI.TwoPointCorrelations.coordinateAssignment, OAI.TwoPointCorrelations.splitAssignment, OAI.TwoPointCorrelations.outsideCoordinates