OAI/MeasureTheory/Falconer/Angular/FactorizedAngularState.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The factorized symbols used by recursive angular states

The descriptor list is part of the type: every descriptor occurs once, with an explicitly recorded jet. Passing to a deeper cell filters that list and keeps the same spatial and smooth angular multipliers.

  1. structure OAI.Falconer.DescriptorJetSymbol line 19
  2. def OAI.Falconer.DescriptorJetSymbol.restrict line 34
  3. def OAI.Falconer.DescriptorJetSymbol.multiplier line 46
  4. theorem OAI.Falconer.DescriptorJetSymbol.multiplier_measurable line 50
  5. theorem OAI.Falconer.DescriptorJetSymbol.multiplier_bound line 55
  6. def OAI.Falconer.DescriptorJetSymbol.value line 65
  7. theorem OAI.Falconer.DescriptorJetSymbol.value_measurable line 74
  8. theorem OAI.Falconer.DescriptorJetSymbol.value_norm_le line 83
  9. theorem OAI.Falconer.DescriptorJetSymbol.value_admissible line 98
  10. theorem OAI.Falconer.DescriptorJetSymbol.endpoint_restrict line 123
  11. theorem OAI.Falconer.DescriptorJetSymbol.energy_remove_reached line 141