OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceWindowBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The large parent reference cone is still inside the B^4 window used by the angular-error estimate. All constants here precede the packet family.

  1. theorem OAI.LipschitzHilbert.SourceParameters.reference_window_budget line 12
  2. theorem OAI.LipschitzHilbert.SourceParameters.branching_eq_two_pow_product line 20
  3. theorem OAI.LipschitzHilbert.SourceParameters.branching_ge_one line 24
  4. theorem OAI.LipschitzHilbert.SourceParameters.exists_reference_window_index line 27
  5. theorem OAI.LipschitzHilbert.SourceParameters.eventually_reference_mask_width line 32