OscillatoryExpansion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Oscillatory spatial expansion before absolute values

The product of an endpoint transform and a conjugate transform is written as the exact two-point integral with displacement phase. The identity uses the original spatial measures and does not assume spatial smoothness.

theorem OAI.Falconer.exponential_mul_conj line 18
theorem OAI.Falconer.endpointTransform_mul_star line 28

theorem OAI.Falconer.endpointTransform_four_point line 61

Source documentation

Equation graph:phase, with four possibly different endpoint laws and with the symbols retained inside the original spatial integral.

theorem endpointTransform_four_point {d : ℕ}
    (μ μ' ν ν' : Measure (Space d))
    [IsFiniteMeasure μ] [IsFiniteMeasure μ'] [IsFiniteMeasure ν] [IsFiniteMeasure ν']
    (M M' P P' : ℝ) (b b' c c' : Space d → Sphere d → ℂ)
    (r : ℝ) (w v : Sphere d) :
    (endpointTransform μ M b r w * endpointTransform ν P c r v) *
      star (endpointTransform μ' M' b' r w * endpointTransform ν' P' c' r v) =
    ((M⁻¹ * M'⁻¹) * (P⁻¹ * P'⁻¹)) •
      ∫ z : (Space d × Space d) × (Space d × Space d),
        Complex.exp (Complex.I * ((r *
          (inner ℝ (w : Space d) (z.1.1-z.1.2) +
           inner ℝ (v : Space d) (z.2.1-z.2.2)) : ℝ) : ℂ)) *
…

Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.endpointTransform