OAI/MeasureTheory/DyadicAvoidance/GridModelStability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.FiniteTableModel.selectorAddress_eq_of_grid_stability line 12

   Source documentation

   Stable geometry preserves the full dependent selector address.

   theorem selectorAddress_eq_of_grid_stability {ι : Type u_ι} {a b : ι → ℕ}
       {M d : ℕ} (bS : Node M d → Fin M → ℕ) {x t : ℝ}
       (hx : x ∈ gridStableCenters a b) (e : ι) (P : Node M d) (i : Fin M)
       {n : ℕ} (hresolution : bS P i ≤ b e) (hindex : a e ≤ n)
       (ht : t ∈ Set.Icc (1 : ℝ) 2) :
       selectorAddress bS P i (x + t * ((2 : ℝ)⁻¹) ^ n) = selectorAddress bS P i x := by
   …

   Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.gridStableCenters, OAI.Problem310.FiniteTableModel.selectorAddress

2. theorem OAI.Problem310.FiniteTableModel.selectorValue_eq_of_grid_stability line 23

   Source documentation

   Therefore every completion of the random tables preserves the earlier selector evaluations at a stable center.

   theorem selectorValue_eq_of_grid_stability {ι : Type u_ι} {a b : ι → ℕ}
       {M d : ℕ} (bS : Node M d → Fin M → ℕ) (ω : SelectorTable bS) {x t : ℝ}
       (hx : x ∈ gridStableCenters a b) (e : ι) (P : Node M d) (i : Fin M)
       {n : ℕ} (hresolution : bS P i ≤ b e) (hindex : a e ≤ n)
       (ht : t ∈ Set.Icc (1 : ℝ) 2) :
       selectorValue bS ω P.val i (x + t * ((2 : ℝ)⁻¹) ^ n) =
         selectorValue bS ω P.val i x := by
   …

   Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.gridStableCenters, OAI.Problem310.FiniteTableModel.selectorValue