OAI/NumberTheory/CubicMoment/Estimates/CompactParameterWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compact smooth parameter family inherits uniform logarithmic weight estimates from its joint derivatives.

  1. lemma OAI.CubicFirstMoment.norm_iteratedFDeriv_slice_le line 12
  2. def OAI.CubicFirstMoment.uniformLogWeights_compactParameter line 32

    Source documentation

    Only compactness of the parameter range, joint smoothness and common support are needed; no Mellin estimate is assumed.

    def uniformLogWeights_compactParameter {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] (K : Set E) (hK : IsCompact K)
    (W : E → ℝ → ℂ) (w : ℝ → ℂ)
    (hw : HasCompactSupport w) (hpos : tsupport w ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ w)
    (hW : ContDiff ℝ ∞ (Function.uncurry W))
    (hsupp : ∀ p ∈ K, Function.support (W p) ⊆ Function.support w) :
    UniformLogWeights (fun p : K => W p) := by
…

    Mentions: OAI.CubicFirstMoment.UniformLogWeights