OAI/NumberTheory/JointDickman/Amplification/AmplificationFirstForm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The first divisor form and its quadratic energy

  1. def OAI.JointDickman.firstFormWeight line 11
  2. def OAI.JointDickman.firstFormInner line 17
  3. def OAI.JointDickman.firstDivisorForm line 27
  4. def OAI.JointDickman.firstFormVolume line 33
  5. def OAI.JointDickman.firstFormEnergy line 37
  6. theorem OAI.JointDickman.amplification_first_form line 42
  7. theorem OAI.JointDickman.firstFormWeight_nonneg line 67
  8. theorem OAI.JointDickman.firstDivisorForm_cauchy line 74

    Source documentation

    The Cauchy step removes the first label from the actual divisor form.

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

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