OAI/Analysis/LipschitzHilbert/Trees/SourceMarkedStop.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual cell marks vanish after the first mass crossing, so passing between the stopped prefix and the complete marked product is exact.

  1. theorem OAI.LipschitzHilbert.source_marked_product_stop line 14
  2. theorem OAI.LipschitzHilbert.reverseMarkedValue_eq_ite line 30

    Source documentation

    The exact mark tested at a point is the mark of its actual grid cell.

    theorem reverseMarkedValue_eq_ite (grid : FiniteLineGrid) (level : ℕ → ℕ)
    (count : ℕ) (marked : ℕ → ℕ → Prop) (beta : ℕ → ℝ → ℝ) (j : ℕ) (x : ℝ) :
    reverseMarkedValue grid level count marked beta j x =
      if marked j (grid.index (level (ShiftedBlocks.reverseIndex count j)) x).val
        then beta j x else 1 := rfl
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.reverseMarkedValue, OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex