OAI/Analysis/LipschitzHilbert/Fourier/FiniteLineCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact intervals underlying the finite line-mesh index maps.

  1. def OAI.LipschitzHilbert.FiniteLineGrid.meshWidth line 13
  2. def OAI.LipschitzHilbert.FiniteLineGrid.cell line 16
  3. theorem OAI.LipschitzHilbert.FiniteLineGrid.meshWidth_pos line 19
  4. theorem OAI.LipschitzHilbert.FiniteLineGrid.index_eq_iff_mem_cell line 22
  5. theorem OAI.LipschitzHilbert.FiniteLineGrid.cell_subset_root line 40
  6. theorem OAI.LipschitzHilbert.FiniteLineGrid.index_fiber_inter_root line 59

    Source documentation

    Restricting the coarse-index fiber to the root gives exactly its half-open mesh interval.

    theorem index_fiber_inter_root (g : FiniteLineGrid) {level : ℕ}
    (hl : level ≤ g.depth) {i : ℕ} (hi : i < g.branching ^ level) :
    {x ∈ g.root | (g.index level x).val = i} = g.cell level i := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid