CheapPathCounting.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.cheapStep_card line 16
def OAI.GammaFPP.fixedStepLists line 19
Source documentation
Includes every actual step list of length n, without a simplicity restriction.
```
noncomputable def fixedStepLists (n : ℕ) : Finset (List Step) :=
…
```
lemma OAI.GammaFPP.mem_fixedStepLists line 22
lemma OAI.GammaFPP.card_fixedStepLists_le line 34
def OAI.GammaFPP.fixedTrailLists line 42
Source documentation
The probability bound uses only the subfamily with distinct undirected edges.
```
noncomputable def fixedTrailLists (p : Vertex) (n : ℕ) : Finset (List Step) := by
…
```
lemma OAI.GammaFPP.mem_fixedTrailLists line 46
lemma OAI.GammaFPP.card_fixedTrailLists_le line 52

lemma OAI.GammaFPP.fixedTrail_event_eq line 58

Source documentation

Exact event equality; there is no hidden restriction to a selected optimizer.

lemma fixedTrail_event_eq {Ω : Type*} (τ : Edge → Ω → ℝ)
    (p : Vertex) (n : ℕ) (t : ℝ) :
    {ω | ∃ ds : List Step, ds.length = n ∧
      ((trace p ds).map traversalEdge).Nodup ∧ pathCost (fun e => τ e ω) p ds ≤ t} =
    {ω | ∃ ds ∈ fixedTrailLists p n, pathCost (fun e => τ e ω) p ds ≤ t} := by
…

Mentions: OAI.GammaFPP.fixedTrailLists

theorem OAI.GammaFPP.GammaEnvironment.cheap_fixed_length_probability line 75

Source documentation

All actual fixed-length trails, with a proved four-way exponential count.

theorem GammaEnvironment.cheap_fixed_length_probability
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (s : ℝ) (hsp : 0 < s) (p : Vertex) (n : ℕ) (t : ℝ) :
    P {ω | ∃ ds : List Step, ds.length = n ∧
      ((trace p ds).map traversalEdge).Nodup ∧ pathCost (fun e => τ e ω) p ds ≤ t} ≤
      ((4 ^ n : ℕ) : ℝ≥0∞) *
        ((ENNReal.ofReal ((rate / (rate + s)) ^ shape)) ^ n /
          ENNReal.ofReal (Real.exp (-s * t))) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment