PositiveFirstFormEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Positive quadratic energy from a surviving mixed correlation

theorem OAI.JointDickman.firstFormEnergy_nonneg line 14

theorem OAI.JointDickman.normalized_energy_lower line 22

Source documentation

The numerical Cauchy estimate with the normalization used for the graph.

theorem normalized_energy_lower {B T δ E V r : ℝ} (hB : 0 < B) (hT : 0 < T)
    (hδ : 0 ≤ δ) (hE : 0 ≤ E) (hr : B*δ ≤ r) (hr0 : 0 ≤ r)
    (hC : r^2 ≤ V*E) (hV : V ≤ 2*B/T) : δ^2/2 ≤ E/(B*T) := by
…

theorem OAI.JointDickman.firstFormEnergy_lower line 35

Source documentation

No bound for the first label is lost in the active Cauchy step.

theorem firstFormEnergy_lower {B T : ℕ} (hB : 0 < B) (hT : 0 < T)
    (L : ℕ) (τ C : ℝ) (u : ℕ → ℝ) (v : ℕ → ℕ → ℝ)
    (g J : ℕ → ℂ) (N : ℕ) {δ : ℝ} (hδ : 0 ≤ δ)
    (hu : ∀ c, 0 ≤ u c) (hg : ∀ m, ‖g m‖ ≤ 1)
    (hv : ∀ a c, v a c ≠ 0 → T*c ≤ a)
    (hfirst : (B : ℝ)*δ ≤ ‖firstDivisorForm B L τ C u v g J N‖)
    (hvol : activeFirstFormVolume B L τ C u T N ≤ 2*(B : ℝ)/(T : ℝ)) :
    δ^2/2 ≤ firstFormEnergy B L τ C u v J N / ((B : ℝ)*T) := by
…

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

theorem OAI.JointDickman.norm_eventually_lower line 49

Source documentation

A nonzero limiting correlation gives an eventual lower bound with room for the later Cauchy estimate.

theorem norm_eventually_lower {f : ℕ → ℂ} {w : ℂ} {δ : ℝ}
    (hδ : 0 < δ) (hw : 2*δ ≤ ‖w‖) (hf : Tendsto f atTop (nhds w)) :
    ∀ᶠ n : ℕ in atTop, δ ≤ ‖f n‖ := by
…