OAI/MeasureTheory/Falconer/Fourier/JointStationaryGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Uniform mixed bounds for the actual stationary chart

The reflection formula preserves norm even when its direction parameter is off the sphere. This permits ambient derivatives in that parameter while the original symbol is evaluated only on sphere points.

  1. theorem OAI.Falconer.poleRotationFormula_eq_reflection line 16
  2. theorem OAI.Falconer.poleRotationFormula_norm line 21
  3. def OAI.Falconer.jointStationaryChart line 26
  4. def OAI.Falconer.jointStationaryRegion line 30
  5. def OAI.Falconer.jointStationaryCompact line 33
  6. theorem OAI.Falconer.jointStationaryRegion_isOpen line 37
  7. theorem OAI.Falconer.jointStationaryCompact_isCompact line 41
  8. theorem OAI.Falconer.jointStationaryCompact_subset line 45
  9. theorem OAI.Falconer.jointStationaryChart_contDiffAt line 54
  10. theorem OAI.Falconer.jointStationaryChart_norm line 62
  11. theorem OAI.Falconer.unmaskedStationaryAmplitude_contDiffAt_region line 68
  12. theorem OAI.Falconer.joint_stationary_geometry_bounds line 75
  13. theorem OAI.Falconer.joint_stationary_amplitude_budget line 89

    Source documentation

    All mixed chart derivatives cost only their total order in the original symbol scale. The direction parameter is differentiated in ambient space.

    theorem joint_stationary_amplitude_budget (m K : ℕ) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ B : Space (m+3) → ℂ,
      ContDiff ℝ ∞ B → ∀ C D : ℝ, 0 ≤ C → 1 ≤ D →
      (∀ j ≤ K, ∀ w : Sphere (m+3), ‖iteratedFDeriv ℝ j B w‖ ≤ C*D^j) →
      ∀ j ≤ K, ∀ z ∈ jointStationaryCompact m,
        ‖iteratedFDeriv ℝ j (unmaskedStationaryAmplitude m B) z‖ ≤ A*C*D^K := by
…

    Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.jointStationaryCompact, OAI.Falconer.unmaskedStationaryAmplitude