DenseCoverCore.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite spatial selection and adapted failure accounting for the dense cover.

theorem OAI.SLEExactGauge.select_disjoint_candidates_and_charge line 15

Source documentation

Extract disjoint candidate disks whose fourfold enlargements cover all candidates, and charge their complete covering cost to one measure.

theorem select_disjoint_candidates_and_charge
    {ι : Type*} (I : Finset ι) (x : ι → ℂ) (r : ι → ℝ)
    (R : ℝ) (hr : ∀ i ∈ I, r i ≤ R)
    (ν : Measure ℂ) (A : Set ℂ)
    (hA : ∀ i ∈ I, closedBall (x i) (r i) ⊆ A)
    (cost : ι → ℝ≥0∞) (C : ℝ≥0∞)
    (hcost : ∀ i ∈ I, cost i ≤ C * ν (closedBall (x i) (r i))) :
    ∃ J : Finset ι, J ⊆ I ∧
      (J : Set ι).PairwiseDisjoint (fun i => closedBall (x i) (r i)) ∧
      (∀ i ∈ I, ∃ j ∈ J,
        closedBall (x i) (r i) ⊆ closedBall (x j) (4 * r j)) ∧
      ∑ j ∈ J, cost j ≤ C * ν A := by
…

theorem OAI.SLEExactGauge.selected_and_missed_cover line 50

Source documentation

Candidate-containing cells and the remaining visited cells together form an actual cover after disjoint spatial selection.

theorem selected_and_missed_cover
    {ι η : Type*} (I J : Finset ι) (M : Finset η)
    (D V : ι → Set ℂ) (Q : η → Set ℂ) (E : Set ℂ)
    (hselect : ∀ i ∈ I, ∃ j ∈ J, D i ⊆ V j)
    (hcell : ∀ z ∈ E, (∃ i ∈ I, z ∈ D i) ∨ ∃ k ∈ M, z ∈ Q k) :
    E ⊆ (⋃ j ∈ J, V j) ∪ ⋃ k ∈ M, Q k := by
…

theorem OAI.SLEExactGauge.adapted_failures_bound line 64

Source documentation

Repeated adapted tests require conditional success bounds, with no independence assumption. All previous failures form a measurable past event.

theorem adapted_failures_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω)
    (F : Filtration ℕ mΩ) (failure : ℕ → Set Ω)
    (hmeas : ∀ n, MeasurableSet[F (n + 1)] (failure n))
    (q : ℝ≥0∞)
    (hstep : ∀ n (B : Set Ω), MeasurableSet[F n] B →
      P (B ∩ failure n) ≤ q * P B) :
    ∀ N : ℕ, P (⋂ n ∈ Finset.range N, failure n) ≤ q ^ N * P univ := by
…