OAI/MeasureTheory/Falconer/Fourier/DescriptorInverseJets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Individual radius normalization in the actual inverse expansion

Every mask retains its own radius and derivative order. The extracted coefficient costs only the largest inverse radius to the total order.

  1. def OAI.Falconer.MaskJetIndex.normalizedValue line 19
  2. theorem OAI.Falconer.MaskJetIndex.value_ofReal line 23
  3. theorem OAI.Falconer.MaskJetIndex.value_eq_inv_radius_normalized line 31
  4. theorem OAI.Falconer.MaskJetIndex.normalizedValue_descriptor line 38
  5. def OAI.Falconer.MaskJetTerm.radiusCoefficient line 52
  6. theorem OAI.Falconer.MaskJetTerm.value_radius_normalized line 55
  7. theorem OAI.Falconer.MaskJetTerm.radiusCoefficient_norm_le line 69
  8. theorem OAI.Falconer.MaskJetTerm.value_radius_endpoint_split line 85
  9. theorem OAI.Falconer.MaskJetExpansion.value_radius_normalized line 116
  10. theorem OAI.Falconer.MaskJetExpansion.localInverseAmplitude_product_radius_jets line 127