ChartNonstationary.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nonstationary integration in the actual normalized chart

The phase is the scalar product with the normalized affine chart, not an abstract phase supplied as a hypothesis. Its higher derivative constants come from tangent_line_phase_derivatives.

theorem OAI.Falconer.tangent_chart_nonstationary line 19

theorem OAI.Falconer.failed_test_chart_nonstationary line 51

Source documentation

One failed perpendicular test selects a single tangent direction for all the point replacements in the same discarded cell--cap term.

theorem failed_test_chart_nonstationary (n : ℕ) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (w d : E) (τ : ℝ), ‖w‖ = 1 → 0 < τ →
      τ < ‖perpendicularPart w d‖ →
      ∃ t : E, ‖t‖ = 1 ∧ inner ℝ w t = 0 ∧
        ∀ (y v : E) (f : ℝ → ℂ), inner ℝ w y = 0 → inner ℝ y t = 0 →
          ‖y‖ ≤ 1 → ContDiff ℝ ∞ f →
          ∀ (C D Λ : ℝ), 0 ≤ C → 1 ≤ D → 0 < Λ →
          ‖v‖ ≤ (τ/4)*D → tsupport f ⊆ Icc (-1 : ℝ) 1 →
          (∀ u ∈ tsupport f, ‖y+u•t‖ ≤ 1 ∧
            ‖v-d‖ + 4*‖y+u•t‖*‖d‖ ≤ τ/2) →
          (∀ k ≤ n, ∀ u ∈ tsupport f, ‖iteratedDeriv k f u‖ ≤ C*D^k) →
          ‖∫ u, phaseOscillator (fun x => inner ℝ (normalizedLine (w+y) t x) v) Λ u * f u‖ ≤
…

Mentions: OAI.Falconer.perpendicularPart, OAI.Falconer.phaseOscillator, OAI.Falconer.normalizedLine