GridConnection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.CrossingBridge.grid_bin_endpoint line 8
lemma OAI.GammaFPP.CrossingBridge.grid_trial_vertex_interval line 18
lemma OAI.GammaFPP.CrossingBridge.grid_interval_localization line 39

theorem OAI.GammaFPP.CrossingBridge.grid_bin_connection line 53

Source documentation

A successful trial and two whole-column tests connect every permitted endpoint pair, with allowance K + 200*shape/rate.

theorem grid_bin_connection (weights : Edge → ℝ) (hweights : ∀ e, 0 ≤ weights e)
    (shape rate b m K : ℝ) (hs : 0 < shape) (hr : 0 < rate) (hK : 100 ≤ K) (X h w l : ℤ) (hl : 0 ≤ l) (j : ℕ)
    (hj : 1 ≤ j) (hw : 1 ≤ w)
    (htrial : ∃ t : Fin (j^2), weights ∈ crossingEvent b m K w l (gridTrialTranslate b X h w t))
    (hleft : (∑ e ∈ transverseIntervalEdges b X (gridIntervalLower h w) (gridIntervalUpper j h w),
      weights e) ≤ 100*shape/rate*(j : ℝ)^2*w)
    (hright : (∑ e ∈ transverseIntervalEdges b (X+l) (gridIntervalLower h w) (gridIntervalUpper j h w),
      weights e) ≤ 100*shape/rate*(j : ℝ)^2*w)
    (r₀ : ℝ) (hbin : (h : ℝ)*w ≤ r₀ ∧ r₀ ≤ ((h : ℝ)+1)*w)
    (p q : Vertex) (hp : p.1=X ∧ |transverse b p-r₀| ≤ 1)
    (hq : q.1=X+l ∧ |transverse b q-r₀| ≤ 1) :
    ∃ ds, p+displacement ds=q ∧ pathCost weights p ds ≤ m*l+(K+200*shape/rate)*(j : ℝ)^2*w ∧
…

Mentions: OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.CrossingBridge.gridTrialTranslate

theorem OAI.GammaFPP.CrossingBridge.gridBinGood_connection line 134

Source documentation

A good bin supplies an attachment-crossing-attachment walk between any prescribed endpoints in the bin, with traversal costs counted with multiplicity.

theorem gridBinGood_connection (weights : Edge → ℝ) (hweights : ∀ e, 0 ≤ weights e)
    (shape rate b m K : ℝ) (hs : 0 < shape) (hr : 0 < rate) (hK : 100 ≤ K)
    (X h w l : ℤ) (hl : 0 ≤ l) (j : ℕ) (hj : 1 ≤ j) (hw : 1 ≤ w)
    (hgood : weights ∈ gridBinGood shape rate b m K X h w l j)
    (r₀ : ℝ) (hbin : (h : ℝ)*w ≤ r₀ ∧ r₀ ≤ ((h : ℝ)+1)*w)
    (p q : Vertex) (hp : p.1=X ∧ |transverse b p-r₀| ≤ 1)
    (hq : q.1=X+l ∧ |transverse b q-r₀| ≤ 1) :
    ∃ ds, p+displacement ds=q ∧
      pathCost weights p ds ≤ m*l+Grid.attachmentAllowance shape rate K*(j : ℝ)^2*w ∧
      PathIn p ds {z | X-l ≤ z.1 ∧ z.1 ≤ X+2*l ∧
        |transverse b z-r₀| ≤ Grid.attachmentAllowance shape rate K*(j : ℝ)^2*w} := by
…

Mentions: OAI.GammaFPP.CrossingBridge.gridBinGood, OAI.GammaFPP.Grid.attachmentAllowance, OAI.GammaFPP.CrossingBridge.PathIn