WindowLocalFactor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.WindowLocalFactor.exists_uniform_window_representatives line 18

Source documentation

Padded equal-length child windows provide a common representative set for all outcomes and all local predicates factoring through their subtree grids. The representatives are selected before the outcome or predicates.

theorem exists_uniform_window_representatives {Ω : Type u_Ω} (M r : ℕ)
    (a B : Fin M → ℕ) (hpadding : ∀ i, B i + 1 ≤ a i + 2 * r)
    (x : ℝ) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc (1 : ℝ) 2) ∧
      R.card ≤ 1 + M * r * 2 ^ (2 * r + 2) ∧
      ∀ t ∈ Set.Icc (1 : ℝ) 2, ∃ t' ∈ R,
        ∀ Q : Ω → Fin M → ℝ → Bool,
          (∀ ω i y z, ⌊(2 : ℝ) ^ (B i + 2) * Int.fract y⌋ =
            ⌊(2 : ℝ) ^ (B i + 2) * Int.fract z⌋ → Q ω i y = Q ω i z) →
          ∀ ω (i : Fin M) (j : Fin r),
            Q ω i (x + t' * ((2 : ℝ)⁻¹) ^ (a i + j.val)) =
…

theorem OAI.Problem310.WindowLocalFactor.exists_window_data_representatives line 48

Source documentation

Canonical window data discharges the padding hypothesis for all nondefault children of an internal node, whose incoming windows have the same length.

theorem exists_window_data_representatives {Ω : Type u_Ω} {M d g r₀ : ℕ}
    (W : WindowData (M + 1) d g r₀) (U : FiniteTableModel.Node M d) (x : ℝ) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc (1 : ℝ) 2) ∧
      R.card ≤ 1 + M * W.r (d - U.val.length) * 2 ^ (2 * W.r (d - U.val.length) + 2) ∧
      ∀ t ∈ Set.Icc (1 : ℝ) 2, ∃ t' ∈ R,
        ∀ Q : Ω → Fin M → ℝ → Bool,
          (∀ ω i y z,
            ⌊(2 : ℝ) ^ (W.bstar (U.val ++ [i.castSucc]) + 2) * Int.fract y⌋ =
            ⌊(2 : ℝ) ^ (W.bstar (U.val ++ [i.castSucc]) + 2) * Int.fract z⌋ →
              Q ω i y = Q ω i z) →
          ∀ ω (i : Fin M) (j : Fin (W.r (d - U.val.length))),
…

Mentions: OAI.Problem310.WindowData, OAI.Problem310.FiniteTableModel.Node

theorem OAI.Problem310.WindowLocalFactor.window_local_predicate_factors line 75

Source documentation

The concrete finite-table local predicate inherits its common grid from WindowData's bound on endpoints of descendant edges.

theorem window_local_predicate_factors {M d g r₀ : ℕ}
    (W : WindowData (M + 1) d g r₀)
    (bS : FiniteTableModel.Node M d → Fin M → ℕ)
    (bT : FiniteTableModel.Leaf M d → ℕ)
    (hbS : ∀ Q j, bS Q j = W.b (Q.val ++ [j.castSucc]))
    (hbT : ∀ L, bT L = W.b L.val)
    (ωS : FiniteTableModel.SelectorTable bS) (ωT : FiniteTableModel.TerminalTable bT)
    (choose : List (FiniteTableModel.Child M) → ℝ → FiniteTableModel.Child M)
    (rule : List (FiniteTableModel.Child M) → (Fin M → Bool) → FiniteTableModel.Child M)
    (hchoose : ∀ Q x, choose Q x = rule Q (fun j => FiniteTableModel.selectorValue bS ωS Q j x))
    (U : FiniteTableModel.Node M d) (i : Fin M) (r : ℕ)
    (hdepth : (U.val ++ [i.castSucc]).length + r = d)
…

Mentions: OAI.Problem310.WindowData, OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.Leaf, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.TerminalTable, OAI.Problem310.FiniteTableModel.Child, OAI.Problem310.FiniteTableModel.selectorValue

theorem OAI.Problem310.WindowLocalFactor.exists_concrete_local_representatives line 126

Source documentation

Complete concrete representative adapter. Here Q is the actual local test, with only its defining equality retained as an input for convenient rewriting. No grid-factorization or numerical span hypotheses remain.

theorem exists_concrete_local_representatives {M d g r₀ : ℕ}
    (W : WindowData (M + 1) d g r₀) (U : FiniteTableModel.Node M d) (x : ℝ)
    (choose : FiniteTableModel.SelectorTable (FiniteTableModel.selectorEndpoints W) →
      List (FiniteTableModel.Child M) → ℝ → FiniteTableModel.Child M)
    (rule : List (FiniteTableModel.Child M) → (Fin M → Bool) → FiniteTableModel.Child M)
    (hchoose : ∀ ωS P y, choose ωS P y = rule P (fun j =>
      FiniteTableModel.selectorValue (FiniteTableModel.selectorEndpoints W) ωS P j y))
    (r : ℕ) (hdepth : ∀ i : Fin M, (U.val ++ [i.castSucc]).length + r = d)
    (Q : (FiniteTableModel.SelectorTable (FiniteTableModel.selectorEndpoints W) ×
      FiniteTableModel.TerminalTable (FiniteTableModel.terminalEndpoints W)) →
        Fin M → ℝ → Bool)
    (hQ : ∀ ω i y, Q ω i y =
…

Mentions: OAI.Problem310.WindowData, OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.selectorEndpoints, OAI.Problem310.FiniteTableModel.Child, OAI.Problem310.FiniteTableModel.selectorValue, OAI.Problem310.FiniteTableModel.TerminalTable, OAI.Problem310.FiniteTableModel.terminalEndpoints