OAI/MeasureTheory/DyadicAvoidance/WindowFixedScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.WindowTrialAddresses.window_fixed_scale_on_center_atom line 20

   Source documentation

   Exact fixed-scale failure mass for the actual W-indexed finite table model. All fresh-selector and adaptive-terminal injectivity obligations are discharged here; local leaves only have to stay in their selected child.

   theorem window_fixed_scale_on_center_atom
       (W : WindowData (M + 1) d g r₀) (P : Node M d) (x t : ℝ)
       (ht : t ∈ Set.Icc (1 : ℝ) 2)
       (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
       (value : Node M d × Fin M → Bool)
       (leaf : SelectorTable (selectorEndpoints W) → LocalTrial W P → Leaf M d)
       (hprefix : ∀ a z, (selectorEdge P z.1).IsPrefix (leaf a z).val) :
       outcomeLaw (SelectorAddress (selectorEndpoints W)) (TerminalAddress (terminalEndpoints W))
         p hp0 hp1
         {z : SelectorTable (selectorEndpoints W) × TerminalTable (terminalEndpoints W) |
           (∀ c : Node M d × Fin M,
             z.1 (selectorAddress (selectorEndpoints W) c.1 c.2 x) = value c) ∧
   …

   Mentions: OAI.Problem310.WindowData, OAI.Problem310.WindowTrialAddresses.LocalTrial