SparseEnvelopeWeights.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed product envelope in the sparse branch gives an actual uniform family of inner weights on every fixed outer norm dyad.

lemma OAI.CubicFirstMoment.scaled_exp_log line 12
def OAI.CubicFirstMoment.UniformLogWeights.logDilate line 18
Source documentation
A bounded logarithmic dilation preserves the given uniform smooth weight bounds. Its support and all derivatives are derived explicitly.
```
def UniformLogWeights.logDilate {γ : Type*} {W : γ → ℝ → ℂ}
    (h : UniformLogWeights W) (D : ℝ) (hD : 0 ≤ D) :
    UniformLogWeights (fun z : γ × {s : ℝ // 0 < s ∧ |Real.log s| ≤ D} =>
      fun x => W z.1 (z.2*x)) := by
…
```
Mentions: OAI.CubicFirstMoment.UniformLogWeights
lemma OAI.CubicFirstMoment.log_dyad_ratio line 58