OAI/Analysis/LipschitzHilbert/Trees/SourcePathCountInvariant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A terminal path is independent of how far the finite hierarchy is extended. Thus the individual terminal counts used by the plane theorem can be replaced by one finite count for every top in a root.

  1. theorem OAI.LipschitzHilbert.firstMassStop_eq_of_terminal line 13
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourceActivePathValue_count_congr line 29
  3. theorem OAI.LipschitzHilbert.AngularGrid.source_common_terminal line 57

    Source documentation

    The maximum of the actual individual terminal counts is terminal for every top in the finite root family.

    theorem source_common_terminal {Kb : ℕ} (g : AngularGrid) (tops : Finset τ)
    (precision : τ → ℝ) (cutoff : ℝ) (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (hKb : 0 < Kb) (shift : Fin Kb) (count : τ → ℕ)
    (hterminal : ∀ t ∈ tops, ¬g.eligible cutoff (precision t) (ShiftedBlocks.endpoint shift (count t))) :
    ∀ t ∈ tops, ¬g.eligible cutoff (precision t)
      (ShiftedBlocks.endpoint shift (tops.sup count)) := by
…

    Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint