OAI/Analysis/LiebThirring/IntervalAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.ActionProof.actionDensity line 29
2. lemma OAI.SharpLiebThirring.ActionProof.actionDensity_continuous line 32
3. lemma OAI.SharpLiebThirring.ActionProof.penalized_action_integral line 40
4. lemma OAI.SharpLiebThirring.ActionProof.mulVec_hasDerivAt line 97
5. lemma OAI.SharpLiebThirring.ActionProof.compact_amplitudes line 103
6. lemma OAI.SharpLiebThirring.ActionProof.regularized_action_upper_test line 117

   Source documentation

   An arbitrary finite upper bound on all triangular actions bounds the endpoint jump. This avoids imposing a finiteness convention on a real-valued supremum.

   lemma regularized_action_upper_test {σ δ l r S : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ < 1)
       (hδ : 0 < δ) (hlr : l ≤ r) (k : Fin N → ℝ) (hk : ∀ i, 0 < k i)
       (u v : ℝ → Fin N → ℝ) (hu : ContinuousOn u (Icc l r)) (hv : ContinuousOn v (Icc l r))
       (hud : ∀ t ∈ Ioo l r, ∀ i, HasDerivAt (fun t ↦ u t i) (v t i) t)
       (hul : u l = 0) (hur : u r = 0)
       (ho : ∀ i j, (∫ t in l..r, u t i*u t j) = if i=j then 1 else 0)
       (hS : ∀ C : LowerSpace N,
         (∫ t in l..r, actionDensity σ k (C.val *ᵥ u t) (C.val *ᵥ v t)) ≤ S) :
       fieldPrimitive σ δ k (-diagonal k) - fieldPrimitive σ δ k (diagonal k) ≤ S := by
   …

   Mentions: OAI.SharpLiebThirring.ActionProof.actionDensity, OAI.SharpLiebThirring.fieldPrimitive

7. lemma OAI.SharpLiebThirring.ActionProof.finite_action_upper_test line 154