MellinWeightFamily.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform Mellin estimates for the smooth weight families occurring in Type I. The hypotheses state common support and derivative bounds in logarithmic coordinates. No transform or moment estimate is assumed.

structure OAI.CubicFirstMoment.UniformLogWeights line 13
def OAI.CubicFirstMoment.uniformLogWeights_constant line 25
Source documentation
A fixed test function, with any index set, has the required uniform support and derivative bounds.
```
def uniformLogWeights_constant {ι : Type*} (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) : UniformLogWeights (fun _ : ι => W) := by
…
```
Mentions: OAI.CubicFirstMoment.UniformLogWeights
lemma OAI.CubicFirstMoment.weight_exp_derivative_bound line 45
lemma OAI.CubicFirstMoment.UniformLogWeights.log_seminorms line 58
lemma OAI.CubicFirstMoment.UniformLogWeights.vertical_bounded line 110

theorem OAI.CubicFirstMoment.UniformLogWeights.mellin_decay line 132

Source documentation

Uniform rapid decay, derived from support and derivative bounds.

theorem UniformLogWeights.mellin_decay {ι : Type*} {W : ι → ℝ → ℂ}
    (h : UniformLogWeights W) (M : ℝ) (A : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ i σ, |σ| ≤ M → ∀ t : ℝ,
      (1+|t|)^A*‖mellin (W i) ((σ:ℂ)+(t:ℂ)*Complex.I)‖ ≤ C := by
…

Mentions: OAI.CubicFirstMoment.UniformLogWeights

lemma OAI.CubicFirstMoment.UniformLogWeights.vertical_seminorms line 148
lemma OAI.CubicFirstMoment.UniformLogWeights.mellin_norm_moment line 159

theorem OAI.CubicFirstMoment.UniformLogWeights.mellin_linear_integral line 186

Source documentation

The common linear Mellin majorant needed for the Type-I Fubini bound.

theorem UniformLogWeights.mellin_linear_integral {ι : Type*} {W : ι → ℝ → ℂ}
    (h : UniformLogWeights W) (M : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ i σ, |σ| ≤ M →
      (∫ t : ℝ, ‖mellin (W i) ((σ:ℂ)+(t:ℂ)*Complex.I)‖*(3+|t|)) ≤ C := by
…

Mentions: OAI.CubicFirstMoment.UniformLogWeights