OAI/MeasureTheory/Falconer/Estimates/SeparatedInverse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite endpoint separation of the actual inverse amplitudes

The finite expansion is constructed from product rules and chart pullbacks. Every factor is globally smooth and depends on one endpoint only. This is an identity for the original masked inverse, with no extra analytic input.

  1. def OAI.Falconer.SmoothSeparation.stationaryJetMultiplier line 21
  2. theorem OAI.Falconer.SmoothSeparation.stationaryJetMultiplier_contDiff line 25
  3. def OAI.Falconer.SmoothSeparation.stationaryJointDensity line 29
  4. theorem OAI.Falconer.SmoothSeparation.stationaryJointDensity_contDiff line 32
  5. def OAI.Falconer.SmoothSeparation.stationaryJet line 36
  6. theorem OAI.Falconer.SmoothSeparation.stationaryJet_value line 44
  7. def OAI.Falconer.SmoothSeparation.inverse line 55
  8. theorem OAI.Falconer.SmoothSeparation.inverse_value line 64
  9. theorem OAI.Falconer.localInverseAmplitude_product_separated line 89

    Source documentation

    The exact finite endpoint expansion used in weighted-shell conversion. No endpoint parameter occurs in the opposite factor, and all angular factors are globally smooth.

    theorem localInverseAmplitude_product_separated (m j : ℕ)
    (B : X → Space (m+3) → ℂ) (C : Y → Space (m+3) → ℂ)
    (hB : ∀ x, ContDiff ℝ ∞ (B x)) (hC : ∀ y, ContDiff ℝ ∞ (C y)) :
    ∃ S : SmoothSeparation X Y (Space (m+3)), ∀ x y e,
      localInverseAmplitude m (fun w => B x w*C y w) j e = S.value x y e := by
…

    Mentions: OAI.Falconer.Space, OAI.Falconer.SmoothSeparation, OAI.Falconer.localInverseAmplitude