ImportedAnalyticInputs #
theorem
HermiteLEAN.local_circle_estimate
(E : Finset ℕ)
(hpos : ∀ n ∈ E, 1 ≤ n)
(c : ℕ → ℂ)
:
circleL2Sq (positiveTrigonometricPolynomial E c) ≤ 144 * ↑E.card * circleRhoNormSq (positiveTrigonometricPolynomial E c)
Imported theorem A: local circle estimate for positive frequencies.
theorem
HermiteLEAN.high_frequency_circle_estimate
(N L : ℕ)
(hN : 1 ≤ N)
(hL : 1 ≤ L)
(c : ℕ → ℂ)
(hband : 1343 * ↑L ^ 2 ≤ ↑N ^ 2)
:
circleL2Sq (positiveTrigonometricPolynomial (frequencyBand N L) c) ≤ 32 * circleRhoNormSq (positiveTrigonometricPolynomial (frequencyBand N L) c)
Imported theorem B: high-frequency circle estimate.
theorem
HermiteLEAN.phase_normalized_orthogonal_reduction
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
(defect : H → ℝ)
(hdefect_nonneg : ∀ (h : H), 0 ≤ defect h)
(f0 : H)
(hf0 : ‖f0‖ = 1)
(C : ℝ)
(hC : 0 < C)
(horth : ∀ (g : H), inner ℂ g f0 = 0 → ‖g‖ ≤ C * defect g)
(hscalar : ∀ (h : H), (inner ℂ h f0).im = 0 → |2 * (inner ℂ h f0).re + ‖h‖ ^ 2| ≤ defect h * (2 + ‖h‖))
(hcompare : ∀ (h : H) (a : ℝ), defect (h - ↑a • f0) ≤ |a| + defect h)
:
Imported theorem C: phase-normalized orthogonal reduction.