OAI/Analysis/LipschitzHilbert/Trees/SourceRestrictedGram.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Schur control of the comparable-scale part of a Gram expansion. The other scale pairs are left for the selected-tree geometric estimate.

  1. theorem OAI.LipschitzHilbert.restricted_gram_energy line 13
  2. theorem OAI.LipschitzHilbert.finite_scale_neighbor_count line 40

    Source documentation

    A bounded interval of integer scale indices has uniformly bounded cardinality, including scales at either endpoint of a finite family.

    theorem finite_scale_neighbor_count {N : ℕ} (i : Fin N) (gap : ℕ) :
    (Finset.univ.filter (fun j : Fin N => |(i.val:ℤ)-(j.val:ℤ)|≤(gap:ℤ))).card≤
      2*gap+1 := by
…
  3. theorem OAI.LipschitzHilbert.comparable_scale_gram_energy line 58