PhaseIntegration.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate integration by parts for the angular localization

For an arbitrary smooth real phase in a sphere chart, coordinate integration by parts gives a scale bound through the reciprocal phase derivative. The transport derivative identities concern functions on the real line and are independent of the ambient sphere dimension.

def OAI.Falconer.phaseOscillator line 19
theorem OAI.Falconer.phaseOscillator_norm line 22
theorem OAI.Falconer.phaseOscillator_hasDerivAt line 26
theorem OAI.Falconer.phase_integration_by_parts line 35
theorem OAI.Falconer.phase_transport_iterate_integral line 80

theorem OAI.Falconer.phase_nonstationary_scale_bound line 102

Source documentation

Uniform coordinate IBP. The reciprocal derivative has size U and derivative scale D; the gain per integration is U*D/Λ.

theorem phase_nonstationary_scale_bound {φ : ℝ → ℝ} {q f : ℝ → ℂ}
    (hφ : ContDiff ℝ ∞ φ) (hq : ContDiff ℝ ∞ q) (hf : ContDiff ℝ ∞ f)
    {a b : ℝ} (hab : a ≤ b) (hs : tsupport f ⊆ Icc a b)
    (hrecip : ∀ x ∈ tsupport f, ((deriv φ x : ℝ) : ℂ) * q x = 1)
    (Q : ℕ → ℝ) (hQ : ∀ k, 0 ≤ Q k)
    {C U D Λ : ℝ} (hC : 0 ≤ C) (hU : 0 ≤ U) (hD : 0 ≤ D) (hΛ : 0 < Λ)
    (n : ℕ)
    (hbq : ∀ k ≤ n, ∀ x ∈ tsupport f, ‖iteratedDeriv k q x‖ ≤ Q k * U * D^k)
    (hbf : ∀ k ≤ n, ∀ x ∈ tsupport f, ‖iteratedDeriv k f x‖ ≤ C * D^k) :
    ‖∫ x, phaseOscillator φ Λ x * f x‖ ≤
      (PlanarFalconer.scaledAngularTransportCost Q n 0 * C * (b-a)) * (U*D/Λ)^n := by
…

Mentions: OAI.Falconer.phaseOscillator, OAI.PlanarFalconer.scaledAngularTransportCost