OAI/MeasureTheory/Falconer/Fourier/JetStateBudgetOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Embedding actual states in the fixed recursive derivative budget

  1. def OAI.Falconer.DescriptorJetSymbol.relax line 13
  2. theorem OAI.Falconer.DescriptorJetSymbol.relax_value line 34
  3. theorem OAI.Falconer.jetStateValues_budget_subset line 43
  4. theorem OAI.Falconer.jetStateEnvelope_budget_mono line 56