TriangularElimination.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Successive elimination for finite product laws and triangular events.

def OAI.TwoPointCorrelations.restoreCoordinate line 14
lemma OAI.TwoPointCorrelations.restoreCoordinate_same line 18
lemma OAI.TwoPointCorrelations.restoreCoordinate_other line 22
lemma OAI.TwoPointCorrelations.restoreCoordinate_update line 27
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_weight_restore line 34
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_one_coordinate line 49
Source documentation
Expose one original independent coordinate, keeping all other variables fixed and retaining their original product law.
```
lemma independent_average_one_coordinate (μ : ι → FiniteLaw A) (i : ι)
    (F : (ι → A) → ℝ) :
    (independent μ).average F =
      (independent (fun j : {j : ι // j ≠ i} => μ j)).average (fun y =>
        (μ i).average (fun a => F (restoreCoordinate i a y))) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average, OAI.TwoPointCorrelations.restoreCoordinate

theorem OAI.TwoPointCorrelations.FiniteLaw.eliminate_coordinate line 74

Source documentation

One elimination step. All retained events ignore the variable being summed; only its own event is charged its conditional probability bound.

theorem eliminate_coordinate [Nonempty A] (μ : ι → FiniteLaw A) (i : ι)
    (E F : (ι → A) → Prop) (δ : ℝ)
    (hE : ∀ x a, E (Function.update x i a) ↔ E x)
    (hF : ∀ x, (μ i).probability (fun a => F (Function.update x i a)) ≤ δ) :
    (independent μ).probability (fun x => E x ∧ F x) ≤
      δ * (independent μ).probability E := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.probability, OAI.TwoPointCorrelations.FiniteLaw.independent

theorem OAI.TwoPointCorrelations.FiniteLaw.triangular_probability_bound line 109

Source documentation

Simultaneous triangular events cost one conditional factor per selected coordinate. The retained earlier events explicitly ignore every later coordinate, including any appearance as a controlling modulus.

theorem triangular_probability_bound [LinearOrder ι] [Nonempty A]
    (μ : ι → FiniteLaw A) (E : ι → (ι → A) → Prop) (δ : ℝ) (hδ : 0 ≤ δ)
    (R : Finset ι)
    (hdepends : ∀ i ∈ R, ∀ j ∈ R, i < j → ∀ x a,
      E i (Function.update x j a) ↔ E i x)
    (hconditional : ∀ i ∈ R, ∀ x,
      (μ i).probability (fun a => E i (Function.update x i a)) ≤ δ) :
    (independent μ).probability (fun x => ∀ i ∈ R, E i x) ≤ δ ^ R.card := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.probability, OAI.TwoPointCorrelations.FiniteLaw.independent