IndependentCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.coordinateMissEvent line 12
Source documentation
The finite union event specifying at least q coordinate misses.
```
def coordinateMissEvent (I : Finset SourceCoordinate) (q : ℕ)
    (S : SourceCoordinate → Set ℝ) : Set (SourceCoordinate → ℝ) :=
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate
theorem OAI.FiniteFactor.coordinateMissEvent_bound line 18
Source documentation
Independence and the union bound, retaining the exact natural exponent. This lemma uses the actual source angle law.
```
theorem coordinateMissEvent_bound (I : Finset SourceCoordinate) (q : ℕ)
    (S : SourceCoordinate → Set ℝ) (hS : ∀ i, MeasurableSet (S i))
    (b : ℝ≥0∞) (hb : ∀ i ∈ I, sourceAngleMarginal i (S i) ≤ b) :
    sourceAngleLaw (coordinateMissEvent I q S) ≤ (2 : ℝ≥0∞)^I.card * b^q := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleMarginal, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.coordinateMissEvent

theorem OAI.FiniteFactor.mem_coordinateMissEvent_of_card line 43

Source documentation

Any realization with at least q misses lies in the union event.

theorem mem_coordinateMissEvent_of_card (I : Finset SourceCoordinate) (q : ℕ)
    (S : SourceCoordinate → Set ℝ) (θ : SourceCoordinate → ℝ)
    (h : q ≤ (I.filter (fun i => θ i ∈ S i)).card) : θ ∈ coordinateMissEvent I q S := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.coordinateMissEvent