ActiveFirstForm.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Restricting the Cauchy volume to the actual multiplier range

def OAI.JointDickman.activeFirstFormWeight line 11
def OAI.JointDickman.activeFirstFormVolume line 15
theorem OAI.JointDickman.firstFormInner_eq_zero_of_inactive line 19
theorem OAI.JointDickman.activeFirstFormWeight_nonneg line 36

theorem OAI.JointDickman.firstDivisorForm_active_cauchy line 46

Source documentation

The Cauchy volume only counts multipliers permitted by the smooth coefficient window, giving the factor 1/(Tc) in its later mean estimate.

theorem firstDivisorForm_active_cauchy (B L : ℕ) (τ C : ℝ) (u : ℕ → ℝ)
    (v : ℕ → ℕ → ℝ) (g J : ℕ → ℂ) (T N : ℕ)
    (hu : ∀ c, 0 ≤ u c) (hg : ∀ m, ‖g m‖ ≤ 1)
    (hv : ∀ a c, v a c ≠ 0 → T*c ≤ a) :
    ‖firstDivisorForm B L τ C u v g J N‖^2 ≤
      activeFirstFormVolume B L τ C u T N * firstFormEnergy B L τ C u v J N := by
…

Mentions: OAI.JointDickman.firstDivisorForm, OAI.JointDickman.activeFirstFormVolume, OAI.JointDickman.firstFormEnergy

theorem OAI.JointDickman.amplificationBump_ratio_lower line 81
Source documentation
The concrete bump has the required lower support condition.
```
theorem amplificationBump_ratio_lower (T a c : ℕ)
    (h : amplificationBump (((a : ℝ) / ((T : ℝ)*c))) ≠ 0) : T*c ≤ a := by
…
```
Mentions: OAI.JointDickman.amplificationBump