UniformCoordinateWeights.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform joint Mellin moments from the actual common support and derivative bounds of the coordinate weights.

lemma OAI.CubicFirstMoment.zeroLineMellinMass_nonneg line 13
lemma OAI.CubicFirstMoment.UniformLogWeights.zeroLine_moment line 17
lemma OAI.CubicFirstMoment.independentMellinMoment_factorization line 29
theorem OAI.CubicFirstMoment.UniformLogWeights.coordinate_moments line 57
Source documentation
One bound controls the product L1 mass and the genuine joint tail moment for every member of a uniformly smooth coordinate family.
```
theorem UniformLogWeights.coordinate_moments {γ : Type*} {W : γ → ι → ℝ → ℂ}
    (h : UniformLogWeights (fun z : γ × ι => W z.1 z.2)) (A : ℕ) :
    ∃ C J : ℝ, 0 ≤ C ∧ 0 ≤ J ∧ ∀ u : γ,
      (∏ i, zeroLineMellinMass (W u i)) ≤ C ∧ independentMellinMoment (W u) A ≤ J := by
…
```
Mentions: OAI.CubicFirstMoment.UniformLogWeights, OAI.CubicFirstMoment.zeroLineMellinMass, OAI.CubicFirstMoment.independentMellinMoment