OrderedElimination.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Eliminate labels in the order of witness records, independently of label names.

theorem OAI.TwoPointCorrelations.FiniteLaw.ordered_coordinate_probability_bound line 17

Source documentation

The order belongs to the relation records. The ambient prime labels need no compatible order and all unselected coordinates keep their law.

theorem ordered_coordinate_probability_bound {κ : Type*} [LinearOrder κ]
    [Nonempty A] (coordinate : κ → ι)
    (μ : ι → FiniteLaw A) (E : κ → (ι → A) → Prop) (δ : ℝ) (hδ : 0 ≤ δ)
    (R : Finset κ)
    (hdepends : ∀ i ∈ R, ∀ j ∈ R, i < j → ∀ x a,
      E i (Function.update x (coordinate j) a) ↔ E i x)
    (hconditional : ∀ i ∈ R, ∀ x,
      (μ (coordinate i)).probability (fun a => E i (Function.update x (coordinate 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

theorem OAI.TwoPointCorrelations.FiniteLaw.ordered_prime_relation_probability line 75

Source documentation

Ordered nondegenerate prime relations: selected coordinates can be any labels in the ambient assignment, not necessarily an initial segment.

theorem ordered_prime_relation_probability {κ : Type*} [LinearOrder κ]
    (τ : κ → Type*) [∀ i, Fintype (τ i)]
    [Nonempty A] (μ : ι → FiniteLaw A) (value : A → ℕ)
    (hinj : Function.Injective value) (H N : ℕ) (hH : 0 < H) (hN : 1 ≤ N)
    (hprime : ∀ a, (value a).Prime) (hlo : ∀ a, H ≤ value a)
    (hhi : ∀ a, value a ≤ N) (hweight : ∀ i a, (μ i).weight a ≤ (value a : ℝ)⁻¹)
    (m : (i : κ) → τ i → PrimeMonomial ι) (selected control : κ → ι) (R : Finset κ)
    (hcontrol : ∀ i ∈ R, control i ≠ selected i)
    (htriangular : ∀ i ∈ R, ∀ j ∈ R, i < j →
      selected j ∉ primeRelationSupport (m i) ∧ control i ≠ selected j) :
    (independent μ).probability (fun x => ∀ i ∈ R,
      primeRelationEvent (m i) (selected i) (control i) (integerPrimeAssignment value x)) ≤
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.PrimeMonomial, OAI.TwoPointCorrelations.primeRelationSupport, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.probability, OAI.TwoPointCorrelations.primeRelationEvent, OAI.TwoPointCorrelations.integerPrimeAssignment