OAI/MeasureTheory/Falconer/Fourier/InverseJetSupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Global original-point factors for the inverse expansion

Every inverse coefficient vanishes off the fixed patch. Thus its individual mask jets can be evaluated at the original sphere point globally, and each resulting descriptor factor retains every original angular good condition.

  1. theorem OAI.Falconer.MaskJetExpansion.stationaryJet_coefficient_eq_zero line 20
  2. theorem OAI.Falconer.MaskJetExpansion.inverse_coefficient_eq_zero line 28
  3. theorem OAI.Falconer.MaskJetExpansion.inverse_product_term_radius_normalized line 46
  4. theorem OAI.Falconer.MaskJetExpansion.localInverseAmplitude_product_radius_jets_global line 65

    Source documentation

    The finite normalized expansion holds everywhere on the sphere.

    theorem localInverseAmplitude_product_radius_jets_global (m j : ℕ)
    (r : ι → ℝ) (hr : ∀ i, r i ≠ 0) (B : ι → X → Space (m+3) → ℝ)
    (hB : ∀ i x, ContDiff ℝ ∞ (B i x)) (x : X) (e : Sphere (m+3)) :
    let T := (product : MaskJetExpansion ι (m+3) (Space (m+3))).inverse m j
…

    Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.MaskJetExpansion.product, OAI.Falconer.MaskJetExpansion, OAI.Falconer.MaskJetExpansion.inverse

  5. theorem OAI.Falconer.MaskJetExpansion.localInverseAmplitude_endpoint_radius_jets_global line 85
  6. def OAI.Falconer.normalizedDescriptorJetFactor line 117
  7. theorem OAI.Falconer.normalizedDescriptorJetFactor_eq_product line 125
  8. theorem OAI.Falconer.normalizedDescriptorJetFactor_support line 134
  9. theorem OAI.Falconer.normalizedDescriptorJetFactor_measurable line 147