OAI/Combinatorics/TreewidthL1/CacheControl.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundedTreewidthL1.near_far_scaled line 8
  2. lemma OAI.BoundedTreewidthL1.protected_threshold_scaled line 49
  3. lemma OAI.BoundedTreewidthL1.protected_of_successor line 71
  4. structure OAI.BoundedTreewidthL1.GeometricTrack line 93

    Source documentation

    Physical, unnormalized data for a single actual root-to-endpoint cache. The probabilistic tests are discharged from the constructed ensemble below.

    structure GeometricTrack (V : Type*) [MetricSpace V] (N : ℕ) (U J H Q : ℝ) where
…
  5. lemma OAI.BoundedTreewidthL1.GeometricTrack.successor_protected line 124
  6. def OAI.BoundedTreewidthL1.GeometricTrack.control line 157