ActionBounds.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SharpLiebThirring.ActionProof.trace_square_real line 25
lemma OAI.SharpLiebThirring.ActionProof.quadratic_swap line 35
lemma OAI.SharpLiebThirring.ActionProof.trace_rankone_mul line 48
lemma OAI.SharpLiebThirring.ActionProof.quadratic_hasDerivAt line 58
def OAI.SharpLiebThirring.SpectralProof.actionYoungConstant line 88
lemma OAI.SharpLiebThirring.SpectralProof.sigma_holderConjugate line 90
lemma OAI.SharpLiebThirring.SpectralProof.young_action_bound line 100
lemma OAI.SharpLiebThirring.SpectralProof.triangular_diagonal_energy_nonpos line 124

lemma OAI.SharpLiebThirring.PathProof.upper_barrier line 145

Source documentation

The endpoint barrier used to remove the field cutoff. No strict negativity or Lipschitz property of the scalar derivative is needed.

lemma upper_barrier {f f' : ℝ → ℝ} {l r κ : ℝ}
    (hc : ContinuousOn f (Icc l r))
    (hd : ∀ x ∈ Icc l r, HasDerivAt f (f' x) x)
    (hl : f l ≤ κ)
    (hb : ∀ x ∈ Icc l r, κ < f x → f' x ≤ 0) :
    ∀ x ∈ Icc l r, f x ≤ κ := by
…

lemma OAI.SharpLiebThirring.PathProof.two_endpoint_barrier line 171
def OAI.SharpLiebThirring.ActionProof.realSelfAdjointEntryCLM line 206
Source documentation
Real entry evaluation on the actual symmetric-matrix normed space.
```
def realSelfAdjointEntryCLM (i j : Fin N) :
    selfAdjoint (Matrix (Fin N) (Fin N) ℝ) →L[ℝ] ℝ :=
…
```
lemma OAI.SharpLiebThirring.ActionProof.realSelfAdjoint_entry_derivative line 218
lemma OAI.SharpLiebThirring.ActionProof.real_rankone_isHermitian line 226

lemma OAI.SharpLiebThirring.ActionProof.action_ode_identity line 232

Source documentation

The exact penalized action identity, pointwise wherever the amplitude is differentiable. Hence it applies to the a.e. derivative of H¹ amplitudes.

lemma action_ode_identity {σ δ ε : ℝ} (hσ : σ < 1) (hδ : 0 < δ) (hε : 0 < ε)
    (k : Fin N → ℝ) {a a' : ℝ → Fin N → ℝ}
    {B : ℝ → selfAdjoint (Matrix (Fin N) (Fin N) ℝ)}
    {B' : selfAdjoint (Matrix (Fin N) (Fin N) ℝ)} {x : ℝ}
    (ha : ∀ i, HasDerivAt (fun t ↦ a t i) (a' x i) x)
    (hB : HasDerivAt B B' x)
    (hode : ε • (B' : Matrix (Fin N) (Fin N) ℝ) =
      matrixField σ δ k (B x) - vecMulVec (a x) (a x)) :
    HasDerivAt (fun t ↦ fieldPrimitive σ δ k (B t) +
      ∑ i, a t i * ((B t : Matrix (Fin N) (Fin N) ℝ) *ᵥ a t) i)
      (2 * (∑ i, a' x i * ((B x : Matrix (Fin N) (Fin N) ℝ) *ᵥ a x) i) -
        constraintDefect σ δ k (B x, a x) / ε) x := by
…

Mentions: OAI.SharpLiebThirring.matrixField, OAI.SharpLiebThirring.fieldPrimitive, OAI.SharpLiebThirring.ActionProof.constraintDefect

lemma OAI.SharpLiebThirring.ActionProof.quadratic_square_real line 264
lemma OAI.SharpLiebThirring.ActionProof.action_pointwise_square_bound line 270
lemma OAI.SharpLiebThirring.ActionProof.action_penalty_pointwise line 280