OAI/Analysis/Littlewood/Curvature.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AsymptoticallyMinimalLittlewood.Curvature.separating_kernel line 13
2. lemma OAI.AsymptoticallyMinimalLittlewood.Curvature.exists_generic line 30
3. lemma OAI.AsymptoticallyMinimalLittlewood.Curvature.exists_kernel_vectors line 39
4. theorem OAI.AsymptoticallyMinimalLittlewood.Curvature.determinant_tuning line 57

   Source documentation

   Given any prescribed positive factors A_i, the products of curvatures can be made simultaneously (1±delta) tau A_i, with all curvatures nonzero. The theorem is used with A_i=|c_i|^2/rho_i.

   theorem determinant_tuning {I : Type uI} {V : Type uV} [Fintype I] [DecidableEq I]
       [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
       (f : I → V →ₗ[ℝ] ℝ) (hf : ∀ i, f i ≠ 0)
       (hpair : ∀ i j, i ≠ j → ∀ c : ℝ, f i ≠ c • f j)
       (A : I → ℝ) (hA : ∀ i, 0 < A i) {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ < 1) :
       ∃ τ : ℝ, 0 < τ ∧ ∃ b : I → V,
         (∀ i j, f i (b j) ≠ 0) ∧
         ∀ i, (1-δ)*τ*A i ≤ ∏ j, |f i (b j)| ∧
           (∏ j, |f i (b j)|) ≤ (1+δ)*τ*A i := by
   …