OAI/Analysis/LiebThirring/ConnectingPath.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.MatrixFlow.state_diagonal_le line 29
2. lemma OAI.SharpLiebThirring.MatrixFlow.sourceField_state_nonpos line 45
3. lemma OAI.SharpLiebThirring.MatrixFlow.source_path_state_barrier line 64
4. lemma OAI.SharpLiebThirring.MatrixFlow.sym_norm_le_of_states line 93
5. lemma OAI.SharpLiebThirring.MatrixFlow.source_connecting_path line 121

   Source documentation

   The connecting path, with one coefficient box for all small penalties. The radial cutoff has been removed by the two endpoint barriers.

   lemma source_connecting_path {σ δ l r : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1) (hδ : 0 < δ)
       (hlr : l ≤ r) (k : Fin N → ℝ) (hk : ∀ i, 0 < k i)
       (u : ℝ → Fin N → ℝ) (hu : ContinuousOn u (Icc l r))
       (ho : ∀ i j, (∫ t in l..r, u t i * u t j) = if i=j then 1 else 0) :
       ∃ R : ℝ, ∀ ε : ℝ, 0 < ε → ε ≤ 1 →
         ∃ (C : LowerSpace N) (X : ℝ → Sym N),
           (∀ i j, |C.val i j| ≤ R) ∧ X l = symDiag k ∧ X r = -symDiag k ∧
           (∀ t ∈ Icc l r, ‖X t‖ ≤ ‖k‖) ∧
           (∀ t ∈ Icc l r, HasDerivWithinAt X
             (ε⁻¹ • (sourceField σ δ hσ₁ hδ k (X t) - symOuter (C.val *ᵥ u t))) (Icc l r) t) := by
   …

   Mentions: OAI.SharpLiebThirring.MatrixFlow.Sym, OAI.SharpLiebThirring.MatrixFlow.symDiag, OAI.SharpLiebThirring.MatrixFlow.sourceField, OAI.SharpLiebThirring.MatrixFlow.symOuter