FiniteBaseCircleEstimate

FiniteBaseCircleEstimate

Finite Fourier-side scaffold for the one-dimensional circle estimate with explicit support and gap parameters.

noncomputable def DimdPolyLEAN.lowPoly {D : ℕ} (q : Fin (D + 1) → ℂ) : AddCircle (2 * Real.pi) → ℂ

lowPoly: low Poly.

Equations

• DimdPolyLEAN.lowPoly q t = ∑ n : Fin (D + 1), q n * DimdPolyLEAN.circleChar (↑n) t

noncomputable def DimdPolyLEAN.bandPoly (N : ℕ) {L : ℕ} (p : Fin L → ℂ) : AddCircle (2 * Real.pi) → ℂ

bandPoly: band Poly.

Equations

• DimdPolyLEAN.bandPoly N p t = ∑ m : Fin L, p m * DimdPolyLEAN.circleChar (N + ↑m) t

noncomputable def DimdPolyLEAN.circleL2Sq (f : AddCircle (2 * Real.pi) → ℂ) : ℝ

circleL2Sq: circle L2 Sq.

Equations

• DimdPolyLEAN.circleL2Sq f = ∫ (t : AddCircle (2 * Real.pi)), ‖f t‖ ^ 2 ∂AddCircle.haarAddCircle

noncomputable def DimdPolyLEAN.defectSq (Q P : AddCircle (2 * Real.pi) → ℂ) : ℝ

defectSq: defect Sq.

Equations

• DimdPolyLEAN.defectSq Q P = ∫ (t : AddCircle (2 * Real.pi)), (‖Q t + P t‖ - ‖Q t‖) ^ 2 ∂AddCircle.haarAddCircle

def DimdPolyLEAN.circleBadConst (D : ℕ) : ℕ

circleBadConst: circle Bad Const.

Equations

• DimdPolyLEAN.circleBadConst D = max 1 (max (82 * D) (2 ^ D - 1))

def DimdPolyLEAN.circleGoodBudget (D : ℕ) : ℕ

circleGoodBudget: circle Good Budget.

Equations

• DimdPolyLEAN.circleGoodBudget D = 64 * DimdPolyLEAN.circleBadConst D

def DimdPolyLEAN.circleGap (D : ℕ) : ℕ

circleGap: circle Gap.

Equations

• DimdPolyLEAN.circleGap D = max 37 (2 * DimdPolyLEAN.circleBadConst D * DimdPolyLEAN.circleGoodBudget D)

def DimdPolyLEAN.circleConst (D : ℕ) : ℝ

circleConst: circle Const.

Equations

• DimdPolyLEAN.circleConst D = 64 * ↑(DimdPolyLEAN.circleGap D) ^ 2

theorem DimdPolyLEAN.circleBadConst_pos (D : ℕ) : 1 ≤ circleBadConst D

theorem DimdPolyLEAN.circleGoodBudget_pos (D : ℕ) : 1 ≤ circleGoodBudget D

theorem DimdPolyLEAN.circleGap_ge_37 (D : ℕ) : 37 ≤ circleGap D

theorem DimdPolyLEAN.circleGap_ge_bad_budget (D : ℕ) : 2 * circleBadConst D * circleGoodBudget D ≤ circleGap D

theorem DimdPolyLEAN.circleGap_pos (D : ℕ) : 1 ≤ circleGap D

theorem DimdPolyLEAN.circleConst_pos (D : ℕ) : 0 < circleConst D

theorem DimdPolyLEAN.circleConst_ge_one (D : ℕ) : 1 ≤ circleConst D

theorem DimdPolyLEAN.thirty_two_le_circleConst (D : ℕ) : 32 ≤ circleConst D

theorem DimdPolyLEAN.finite_base_circle_estimate (D : ℕ) {L N : ℕ} : 1 ≤ L → circleGap D * L ≤ N → ∀ (q : Fin (D + 1) → ℂ) (p : Fin L → ℂ), circleL2Sq (bandPoly N p) ≤ circleConst D * defectSq (lowPoly q) (bandPoly N p)

theorem DimdPolyLEAN.finite_base_circle_estimate_exists (D : ℕ) : ∃ (A : ℕ), 1 ≤ A ∧ ∃ (C : ℝ), 0 < C ∧ ∀ {L N : ℕ}, 1 ≤ L → A * L ≤ N → ∀ (q : Fin (D + 1) → ℂ) (p : Fin L → ℂ), circleL2Sq (bandPoly N p) ≤ C * defectSq (lowPoly q) (bandPoly N p)