FiniteBaseAnnulusEstimate

FiniteBaseAnnulusEstimate

Finite annulus-side transfer theorem for a normalized base point in Pkappa.

theorem DimdPolyLEAN.finite_base_product_annulus_estimate {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF : basePointNormalized F) (eps : ℝ) : 0 < eps → ∃ (J : ℕ) (M : ℕ), 1 ≤ M ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (G : Pkappa d kappa), highAnnulusMass J (ofPkappa kappa G) ≤ C * defect F G ^ 2 + eps * ‖G‖ ^ 2

theorem DimdPolyLEAN.finite_base_annulus_estimate {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF : basePointNormalized F) (eps : ℝ) : 0 < eps → ∃ (J : ℕ) (C : ℝ), 0 < C ∧ ∀ {H : Pkappa d kappa} {t eta : ℝ}, ‖H‖ = 1 → 0 < t → t ≤ 4 → 0 ≤ eta → defect F (t • H) ≤ eta * t → highAnnulusMass J (ofPkappa kappa H) ≤ C * eta ^ 2 + eps

theorem DimdPolyLEAN.highAnnulusControl {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF_ne : F ≠ 0) (hF_norm : ‖F‖ = 1) : ∃ (J : ℕ) (delta_high : ℝ), 0 < delta_high ∧ ∀ {H : Pkappa d kappa} {t : ℝ}, orthogonalToPk F H → ‖H‖ = 1 → 0 < t → t ≤ 4 → defect F (t • H) ≤ delta_high * t → highAnnulusMass J (ofPkappa kappa H) ≤ 1 / 4