OAI/Probability/GammaPassage/GridAttachments.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.Grid.verticalExponent line 11
2. def OAI.GammaFPP.Grid.attachmentAllowance line 12
3. lemma OAI.GammaFPP.Grid.verticalExponent_pos line 14
4. lemma OAI.GammaFPP.Grid.attachmentAllowance_ge_fifty line 23

   Source documentation

   The attachment allowance dominates the geometric bound of fifty.

   lemma attachmentAllowance_ge_fifty {shape rate K : ℝ}
       (hs : 0 < shape) (hr : 0 < rate) (hK : 100 ≤ K) :
       50 ≤ attachmentAllowance shape rate K := by
   …

   Mentions: OAI.GammaFPP.Grid.attachmentAllowance

5. theorem OAI.GammaFPP.Grid.vertical_edgeSet_tail line 34

   Source documentation

   Exponential cost tail for an edge set of cardinality at most 50*L.

   theorem vertical_edgeSet_tail (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate) (S : Finset Edge) (L : ℝ)
       (hcard : (S.card : ℝ) ≤ 50 * L) :
       P.real {ω | 100 * shape / rate * L < edgeSum S τ ω} ≤
         Real.exp (-verticalExponent shape * L) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.edgeSum, OAI.GammaFPP.Grid.verticalExponent

6. def OAI.GammaFPP.Grid.binGood line 77

   Source documentation

   Finite-bin event with crossing trials and two whole attachment edge sets.

   def binGood {ι : Type*} (trials : Finset ι) (A : ι → Set (Edge → ℝ))
       (S₁ S₂ : Finset Edge) (shape rate L : ℝ) : Set (Edge → ℝ) :=
   …

7. theorem OAI.GammaFPP.Grid.bin_failure_bound line 84

   Source documentation

   Failure bound from disjoint crossing trials and Gamma attachment tails.

   theorem bin_failure_bound (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate) {ι : Type*}
       (trials : Finset ι) (A : ι → Set (Edge → ℝ)) (supports : ι → Finset Edge)
       (hA : ∀ i ∈ trials, MeasurableSet (A i))
       (hdep : ∀ i ∈ trials, DependsOnEdges (A i) (supports i))
       (hdis : Set.Pairwise (↑trials : Set ι) (fun i j => Disjoint (supports i) (supports j)))
       (q : ℝ) (hq : ∀ i ∈ trials, q ≤ P.real {ω | (fun e => τ e ω) ∈ A i})
       (S₁ S₂ : Finset Edge) (L : ℝ)
       (hc₁ : (S₁.card : ℝ) ≤ 50 * L) (hc₂ : (S₂.card : ℝ) ≤ 50 * L) :
       P.real {ω | (fun e => τ e ω) ∉ binGood trials A S₁ S₂ shape rate L} ≤
         (1-q)^trials.card + 2 * Real.exp (-verticalExponent shape * L) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.Grid.DependsOnEdges, OAI.GammaFPP.Grid.binGood, OAI.GammaFPP.Grid.verticalExponent

8. lemma OAI.GammaFPP.Grid.combined_cost line 122

   Source documentation

   Combined crossing and attachment cost bound.

   lemma combined_cost {shape rate K m l L a b c : ℝ}
       (ha : a ≤ m*l+K*L) (hb : b ≤ 100*shape/rate*L)
       (hc : c ≤ 100*shape/rate*L) :
       a+b+c ≤ m*l+attachmentAllowance shape rate K*L := by
   …

   Mentions: OAI.GammaFPP.Grid.attachmentAllowance

9. theorem OAI.GammaFPP.Grid.transverse_interval_tail line 134

   Source documentation

   Column interval used for vertical attachments.

   theorem transverse_interval_tail (henv : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate)
       (b : ℝ) (X h w : ℤ) (j : ℕ) (hj : 1 ≤ j) (hw : 1 ≤ w) :
       P.real {ω | 100*shape/rate*(j : ℝ)^2*w <
         edgeSum (transverseIntervalEdges b X (gridIntervalLower h w)
           (gridIntervalUpper j h w)) τ ω} ≤
         Real.exp (-verticalExponent shape*(j : ℝ)^2*w) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.edgeSum, OAI.GammaFPP.Grid.transverseIntervalEdges, OAI.GammaFPP.Grid.gridIntervalLower, OAI.GammaFPP.Grid.gridIntervalUpper, OAI.GammaFPP.Grid.verticalExponent

10. theorem OAI.GammaFPP.Grid.source_bin_failure_bound line 148

    Source documentation

    Failure bound for j² separated translated trials and the left and right vertical attachment intervals.

    theorem source_bin_failure_bound (henv : GammaEnvironment shape rate P τ)
        (hs : 0 < shape) (hr : 0 < rate) (b : ℝ) (X h w l : ℤ)
        (j : ℕ) (hj : 1 ≤ j) (hw : 1 ≤ w)
        (A : Fin (j^2) → Set (Edge → ℝ)) (supports : Fin (j^2) → Finset Edge)
        (hA : ∀ i, MeasurableSet (A i))
        (hdep : ∀ i, DependsOnEdges (A i) (supports i))
        (hdis : Pairwise (fun i k => Disjoint (supports i) (supports k)))
        (q : ℝ) (hq : ∀ i, q ≤ P.real {ω | (fun e => τ e ω) ∈ A i}) :
        P.real {ω | (fun e => τ e ω) ∉ binGood Finset.univ A
          (transverseIntervalEdges b X (gridIntervalLower h w) (gridIntervalUpper j h w))
          (transverseIntervalEdges b (X+l) (gridIntervalLower h w) (gridIntervalUpper j h w))
          shape rate ((j : ℝ)^2*w)} ≤
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.Grid.DependsOnEdges, OAI.GammaFPP.Grid.binGood, OAI.GammaFPP.Grid.transverseIntervalEdges, OAI.GammaFPP.Grid.gridIntervalLower, OAI.GammaFPP.Grid.gridIntervalUpper

11. theorem OAI.GammaFPP.Grid.finite_bins_failure_bound line 173

    Source documentation

    Simultaneous finite-bin event, with failure controlled without independence between bins. Only independence of each bin's separated crossing trials is used.

    theorem finite_bins_failure_bound (henv : GammaEnvironment shape rate P τ)
        (hs : 0 < shape) (hr : 0 < rate) {κ : Type*} (bins : Finset κ)
        (j : ℕ) (L : ℝ) (q : ℝ)
        (A : κ → Fin (j^2) → Set (Edge → ℝ))
        (supports : κ → Fin (j^2) → Finset Edge) (S₁ S₂ : κ → Finset Edge)
        (hA : ∀ k ∈ bins, ∀ i, MeasurableSet (A k i))
        (hdep : ∀ k ∈ bins, ∀ i, DependsOnEdges (A k i) (supports k i))
        (hdis : ∀ k ∈ bins, Pairwise (fun i t => Disjoint (supports k i) (supports k t)))
        (hq : ∀ k ∈ bins, ∀ i, q ≤ P.real {ω | (fun e => τ e ω) ∈ A k i})
        (hc₁ : ∀ k ∈ bins, ((S₁ k).card : ℝ) ≤ 50*L)
        (hc₂ : ∀ k ∈ bins, ((S₂ k).card : ℝ) ≤ 50*L) :
        P.real (⋃ k ∈ bins, {ω | (fun e => τ e ω) ∉
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.Grid.DependsOnEdges