IndependentSampling.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Product sampling and the atom bound for independent linear equations.

def OAI.TwoPointCorrelations.joinCoordinates line 15
lemma OAI.TwoPointCorrelations.joinCoordinates_mem line 19
lemma OAI.TwoPointCorrelations.joinCoordinates_notMem line 23
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_probability_all line 30
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_weight_join line 42
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_split line 56
Source documentation
Conditioning on coordinates outside S leaves the original product law on S.
```
lemma independent_average_split (μ : ι → FiniteLaw A) (S : Finset ι) (f : (ι → A) → ℝ) :
    (independent μ).average f =
      (independent (fun i : {i // i ∉ S} => μ i)).average (fun y =>
        (independent (fun i : S => μ i)).average (fun x => f (joinCoordinates S x y))) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average, OAI.TwoPointCorrelations.joinCoordinates
theorem OAI.TwoPointCorrelations.FiniteLaw.probability_le_of_determined_coordinates line 78
Source documentation
An event that determines the coordinates in S, after all other coordinates are fixed, has probability at most α ^ #S.
```
theorem probability_le_of_determined_coordinates (μ : ι → FiniteLaw A)
    (S : Finset ι) (α : ℝ) (hα : 0 ≤ α) (hatom : ∀ i x, (μ i).weight x ≤ α)
    (E : (ι → A) → Prop)
    (hunique : ∀ x y, E x → E y → (∀ i ∉ S, x i = y i) → x = y) :
    (independent μ).probability E ≤ α ^ S.card := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.probability

theorem OAI.TwoPointCorrelations.FiniteLaw.probability_linear_equations line 102

Source documentation

Independent bounded atoms satisfy the expected codimension bound for every surjective real linear system.

theorem probability_linear_equations {K κ : Type*} [Field K] [Fintype κ]
    (μ : ι → FiniteLaw A) (val : A → K) (hval : Function.Injective val)
    (T : (ι → K) →ₗ[K] (κ → K)) (hT : Function.Surjective T)
    (b : κ → K) (α : ℝ) (hα : 0 ≤ α) (hatom : ∀ i x, (μ i).weight x ≤ α) :
    (independent μ).probability (fun x => T (fun i => val (x i)) = b) ≤
      α ^ Fintype.card κ := by
…

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