LongPrimeWeights.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual cutoff weights on a free long prime. Their variation depends on its dyadic ratio and Mellin height, not on the cutoff scales.

lemma OAI.CubicFirstMoment.radial_mellin_interval_variation line 14
lemma OAI.CubicFirstMoment.primeDetectorCutoff_rescaled_smooth line 65
lemma OAI.CubicFirstMoment.primeDetectorCutoff_rescaled_norm line 69
lemma OAI.CubicFirstMoment.primeDetectorCutoff_rescaled_deriv line 74
theorem OAI.CubicFirstMoment.long_prime_cutoff_variation line 88
Source documentation
The same constant works for every cutoff scale. This is the actual selected-bin prime weight, including any permitted norm twist.
```
theorem long_prime_cutoff_variation :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (c P R a b u : ℝ), 0 < c → 0 < P → 1 ≤ R →
      P ≤ a → a ≤ b → b ≤ R*P →
      let f := fun t => (primeDetectorCutoff (t/c):ℂ)*mellinPhase u t
…
```
Mentions: OAI.CubicFirstMoment.primeDetectorCutoff, OAI.CubicFirstMoment.mellinPhase