MetaplecticTwistedTransform.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The norm twist in the original Voronoi formula is exactly the translated Mellin variable in the shifted transform.

lemma OAI.CubicFirstMoment.phaseWeight_compact line 13
lemma OAI.CubicFirstMoment.phaseWeight_positive line 16
lemma OAI.CubicFirstMoment.phaseWeight_smooth line 20
lemma OAI.CubicFirstMoment.mellin_mul_phase line 39
theorem OAI.CubicFirstMoment.metaplecticTransform_twisted line 53
Source documentation
Exact scalar identity. Its outside phase has modulus one.
```
theorem metaplecticTransform_twisted (ℓ : ℤ) (W : ℝ → ℂ)
    (σ : ℝ) {v : ℝ} (hv : 0 < v) (t : ℝ) :
    metaplecticTransform ℓ (fun x => W x*mellinPhase t x) σ v =
      mellinPhase (-t) v*metaplecticShiftTransform ℓ W (-σ) v t := by
…
```
Mentions: OAI.CubicFirstMoment.metaplecticTransform, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.metaplecticShiftTransform

theorem OAI.CubicFirstMoment.metaplecticTransform_twisted_far_left line 89

Source documentation

The original twisted transform has the sharp far-left bound.

theorem metaplecticTransform_twisted_far_left (ℓ : ℤ) (m : ℕ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ v : ℝ, 0 < v → ∀ t : ℝ,
      ‖metaplecticTransform ℓ (fun x => W x*mellinPhase t x) ((m:ℝ)-1/2) v‖ ≤
        C*v^(1/2-(m:ℝ))*(1+|t|)^(4*m) := by
…

Mentions: OAI.CubicFirstMoment.metaplecticTransform, OAI.CubicFirstMoment.mellinPhase