Source declarations with compiler docstrings and elaborated types, including all actual implicit parameters and inherited hypotheses. Definition and structure bodies are also shown. Generated auxiliary declarations are not listed.
Dependency graph of the paper-level results (interactive)
GPDYS/Basic.lean — Sections 2, 3.1–3.3 (definitions and constants)L²) inner product ⟪u, v⟫_h = ∑ᵢ wᵢ uᵢ vᵢ.def winner (w : ι → ℝ) (u v : ι → ℝ) : ℝ := ∑ i, w i * (u i * v i)GPDYS.winner :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₂² = ∑ᵢ wᵢ vᵢ².def wnorm2sq (w : ι → ℝ) (v : ι → ℝ) : ℝ := winner w v vGPDYS.wnorm2sq :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₂ = (∑ᵢ wᵢ vᵢ²)^{1/2}.def wnorm2 (w : ι → ℝ) (v : ι → ℝ) : ℝ := Real.sqrt (wnorm2sq w v)GPDYS.wnorm2 :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₃³ = ∑ᵢ wᵢ |vᵢ|³.def wnorm3p3 (w : ι → ℝ) (v : ι → ℝ) : ℝ := ∑ i, w i * |v i| ^ 3GPDYS.wnorm3p3 :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₄⁴ = ∑ᵢ wᵢ vᵢ⁴.def wnorm4p4 (w : ι → ℝ) (v : ι → ℝ) : ℝ := ∑ i, w i * v i ^ 4GPDYS.wnorm4p4 :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₆⁶ = ∑ᵢ wᵢ vᵢ⁶.def wnorm6p6 (w : ι → ℝ) (v : ι → ℝ) : ℝ := ∑ i, w i * v i ^ 6GPDYS.wnorm6p6 :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₃ = (∑ᵢ wᵢ |vᵢ|³)^{1/3}.def wnorm3 (w : ι → ℝ) (v : ι → ℝ) : ℝ := (wnorm3p3 w v) ^ ((1 : ℝ) / 3)GPDYS.wnorm3 :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₆ = (∑ᵢ wᵢ vᵢ⁶)^{1/6}.def wnorm6 (w : ι → ℝ) (v : ι → ℝ) : ℝ := (wnorm6p6 w v) ^ ((1 : ℝ) / 6)GPDYS.wnorm6 :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → (ι → ℝ) → ℝCS across a family of meshes:
* w are the quadrature weights (the lumped mass matrix is M = diag w), all positive;
* S is the stiffness matrix: symmetric, positive semidefinite, with nonpositive off-diagonal
entries, and such that (M + γ S)⁻¹ has strictly positive entries for every γ > 0
(Lemma 2.2 (ii), a consequence of M + γ S being an irreducible Stieltjes matrix);
* V ≥ 0 is the potential at the nodes and β > 0 the coupling constant;
* CS is the constant of the discrete Sobolev inequality ‖v‖₆ ≤ C_S ‖v‖_{1,h}
(Lemma 2.2 (iii)), where ‖v‖²_{1,h} = ⟪v, -Δ_h v⟫_h + ‖v‖₂² = vᵀ S v + ‖v‖₂².structure Setting (ι : Type*) [Fintype ι] [DecidableEq ι] where
/-- quadrature weights -/
w : ι → ℝ
w_pos : ∀ i, 0 < w i
/-- stiffness matrix -/
S : Matrix ι ι ℝ
S_symm : S.IsSymm
S_psd : ∀ v : ι → ℝ, 0 ≤ v ⬝ᵥ (S *ᵥ v)
S_offdiag : ∀ i j, i ≠ j → S i j ≤ 0
/-- `(M + γ S)⁻¹` has strictly positive entries for every `γ > 0` -/
resolvent_pos : ∀ γ : ℝ, 0 < γ → ∀ i j, 0 < (Matrix.diagonal w + γ • S)⁻¹ i j
/-- potential -/
V : ι → ℝ
V_nonneg : ∀ i, 0 ≤ V i
/-- coupling constant -/
β : ℝ
β_pos : 0 < β
/-- Sobolev constant -/
CS : ℝ
sobolev : ∀ v : ι → ℝ, wnorm6 w v ≤ CS * Real.sqrt (v ⬝ᵥ (S *ᵥ v) + wnorm2sq w v)GPDYS.Setting :
(ι : Type u_2) → [Fintype ι] → [DecidableEq ι] → Type u_2M = diag(w).def M : Matrix ι ι ℝ := Matrix.diagonal P.wGPDYS.Setting.M :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → Matrix ι ι ℝ⟪u, v⟫_h = uᵀ M v.def inner (u v : ι → ℝ) : ℝ := winner P.w u vGPDYS.Setting.inner :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖₂².def nrm2sq (v : ι → ℝ) : ℝ := wnorm2sq P.w vGPDYS.Setting.nrm2sq :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝ‖v‖₂.def nrm2 (v : ι → ℝ) : ℝ := wnorm2 P.w vGPDYS.Setting.nrm2 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝ-Δ_h = M⁻¹ S.def negLap (v : ι → ℝ) : ι → ℝ := fun i => (P.S *ᵥ v) i / P.w iGPDYS.Setting.negLap :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ι → ℝ⟪v, -Δ_h v⟫_h = vᵀ S v.def kin (v : ι → ℝ) : ℝ := v ⬝ᵥ (P.S *ᵥ v)GPDYS.Setting.kin :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝ⟪V v, v⟫_h.def pot (v : ι → ℝ) : ℝ := ∑ i, P.w i * (P.V i * v i ^ 2)GPDYS.Setting.pot :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝH(v) = ½ ⟪V v, v⟫_h + (β/4) ‖v‖₄⁴ of the energy.def H (v : ι → ℝ) : ℝ := (1 / 2) * P.pot v + P.β / 4 * wnorm4p4 P.w vGPDYS.Setting.H :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝE_h(v) = ½ ⟪v, -Δ_h v⟫_h + ½ ⟪V v, v⟫_h + (β/4) ‖v‖₄⁴.def energy (v : ι → ℝ) : ℝ := (1 / 2) * P.kin v + P.H vGPDYS.Setting.energy :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝn(v) = V v + β v³ of the gradient.def nonlin (v : ι → ℝ) : ι → ℝ := fun i => P.V i * v i + P.β * v i ^ 3GPDYS.Setting.nonlin :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ι → ℝ∇E_h(v) = -Δ_h v + n(v) with respect to ⟪·,·⟫_h.def gradE (v : ι → ℝ) : ι → ℝ := P.negLap v + P.nonlin vGPDYS.Setting.gradE :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ι → ℝλ(v) = ⟪∇E_h(v), v⟫_h.def lam (v : ι → ℝ) : ℝ := P.inner (P.gradE v) vGPDYS.Setting.lam :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝg(v) = ∇E_h(v) - λ(v) v.def g (v : ι → ℝ) : ι → ℝ := P.gradE v - P.lam v • vGPDYS.Setting.g :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ι → ℝn: n'(v) = V + 3 β diag(v²), applied to a vector.def nonlin' (v d : ι → ℝ) : ι → ℝ := fun i => (P.V i + 3 * P.β * v i ^ 2) * d iGPDYS.Setting.nonlin' :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → (ι → ℝ) → ι → ℝG_X = I - γ Δ_h, applied to a vector.def GX (γ : ℝ) (v : ι → ℝ) : ι → ℝ := v + γ • P.negLap vGPDYS.Setting.GX :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ι → ℝG_X⁻¹ = (M + γ S)⁻¹ M, applied to a vector.def resolvent (γ : ℝ) (v : ι → ℝ) : ι → ℝ := (P.M + γ • P.S)⁻¹ *ᵥ (P.M *ᵥ v)GPDYS.Setting.resolvent :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ι → ℝX-inner product ⟪v, w⟫_X = ⟪v, G_X⁻¹ w⟫_h.def innerX (γ : ℝ) (v w : ι → ℝ) : ℝ := P.inner v (P.resolvent γ w)GPDYS.Setting.innerX :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → (ι → ℝ) → ℝ‖v‖_X².def nrmXsq (γ : ℝ) (v : ι → ℝ) : ℝ := P.innerX γ v vGPDYS.Setting.nrmXsq :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℝ‖v‖_𝒢² = ⟪v, G_X v⟫_h = ‖v‖₂² + γ ⟪v, -Δ_h v⟫_h.def nrmGsq (γ : ℝ) (v : ι → ℝ) : ℝ := P.nrm2sq v + γ * P.kin vGPDYS.Setting.nrmGsq :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℝu = z / ‖z‖₂ for z ≠ 0; at zero this total function is zero.def normalize (z : ι → ℝ) : ι → ℝ := (P.nrm2 z)⁻¹ • zGPDYS.Setting.normalize :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ι → ℝ𝐱 = G_X⁻¹ (2u - z - γ n(u)) of (DYS I).def xi (γ : ℝ) (z : ι → ℝ) : ι → ℝ :=
P.resolvent γ ((2 : ℝ) • P.normalize z - z - γ • P.nonlin (P.normalize z))GPDYS.Setting.xi :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ι → ℝz ↦ z⁺ = z + 𝐱 - u of the scheme (DYS I), (1.6) in the paper.def step (γ : ℝ) (z : ι → ℝ) : ι → ℝ := z + P.xi γ z - P.normalize zGPDYS.Setting.step :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ι → ℝR(z) = ‖z‖₂ - 1 + γ λ(u).def R (γ : ℝ) (z : ι → ℝ) : ℝ := P.nrm2 z - 1 + γ * P.lam (P.normalize z)GPDYS.Setting.R :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℝ𝓛(z) = E_h(u) + R(z)² / γ.def lyap (γ : ℝ) (z : ι → ℝ) : ℝ := P.energy (P.normalize z) + (P.R γ z) ^ 2 / γGPDYS.Setting.lyap :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℝz^k, started from z⁰ = u⁰.def iter (γ : ℝ) (u0 : ι → ℝ) (k : ℕ) : ι → ℝ := (P.step γ)^[k] u0GPDYS.Setting.iter :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℕ → ι → ℝu^k = z^k / ‖z^k‖₂.def uiter (γ : ℝ) (u0 : ι → ℝ) (k : ℕ) : ι → ℝ := P.normalize (P.iter γ u0 k)GPDYS.Setting.uiter :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℕ → ι → ℝw_min = minᵢ wᵢ when ι is nonempty; the empty-index value is zero.def wmin : ℝ := ⨅ i, P.w iGPDYS.Setting.wmin :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ‖V‖_∞ = maxᵢ Vᵢ on a nonempty mesh (recall V ≥ 0); zero for empty ι.def Vinf : ℝ := ⨆ i, P.V iGPDYS.Setting.Vinf :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝΛ_d = maxᵢ Sᵢᵢ / wᵢ on a nonempty mesh; zero for empty ι.def Λd : ℝ := ⨆ i, P.S i i / P.w iGPDYS.Setting.Λd :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝE₀ = E_h(u⁰) + λ(u⁰)² / max{1, 128 E_h(u⁰)}, (3.9).def E0 (u0 : ι → ℝ) : ℝ := P.energy u0 + (P.lam u0) ^ 2 / max 1 (128 * P.energy u0)GPDYS.Setting.E0 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝP₀ = C_S² (2E₀ + 1), (3.10).def P0 (u0 : ι → ℝ) : ℝ := P.CS ^ 2 * (2 * P.E0 u0 + 1)GPDYS.Setting.P0 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝU₀ = min{1/w_min, P₀/w_min^{1/3}, 2 √(E₀/(β w_min))}, (3.10).def U0 (u0 : ι → ℝ) : ℝ :=
min (1 / P.wmin) (min (P.P0 u0 / P.wmin ^ ((1 : ℝ) / 3))
(2 * Real.sqrt (P.E0 u0 / (P.β * P.wmin))))GPDYS.Setting.U0 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝB₀ = ‖V‖_∞ + β min{P₀^{3/2}, U₀}, (3.11).def B0 (u0 : ι → ℝ) : ℝ := P.Vinf + P.β * min ((P.P0 u0) ^ ((3 : ℝ) / 2)) (P.U0 u0)GPDYS.Setting.B0 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝD = E₀ + B₀, (3.11).def D (u0 : ι → ℝ) : ℝ := P.E0 u0 + P.B0 u0GPDYS.Setting.D :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝB₁ = ‖V‖_∞ + β U₀, (3.11).def B1 (u0 : ι → ℝ) : ℝ := P.Vinf + P.β * P.U0 u0GPDYS.Setting.B1 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝC₀ = 3 β C_S P₀, (3.12).def C0 (u0 : ι → ℝ) : ℝ := 3 * P.β * P.CS * P.P0 u0GPDYS.Setting.C0 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝL₀ = ‖V‖_∞ + min{3 β U₀, C₀ + 2 max{C₀ - 1/4, 0}²}, (3.12).def L0 (u0 : ι → ℝ) : ℝ :=
P.Vinf + min (3 * P.β * P.U0 u0) (P.C0 u0 + 2 * (max (P.C0 u0 - 1 / 4) 0) ^ 2)GPDYS.Setting.L0 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝγ_max = min{1, 1/(128 D), 1/(8 L₀), 2/(B₁ + √(B₁² + 12 D Λ_d))}, (3.14).def γmax (u0 : ι → ℝ) : ℝ :=
min 1 (min (1 / (128 * P.D u0)) (min (1 / (8 * P.L0 u0))
(2 / (P.B1 u0 + Real.sqrt ((P.B1 u0) ^ 2 + 12 * P.D u0 * P.Λd)))))GPDYS.Setting.γmax :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝγ is supplied separately in the theorems using these conditions.def Conditions (u0 : ι → ℝ) (γ : ℝ) : Prop :=
γ ≤ 1 ∧ γ * P.D u0 ≤ 1 / 128 ∧ γ * P.L0 u0 ≤ 1 / 8 ∧
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1GPDYS.Setting.Conditions :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝ → PropGPDYS/Lemmas.lean — Section 3.1 (basic identities)GPDYS.sq_le_of_psd :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : _root_.Module ℝ E] (B : E → E → ℝ),
(∀ (u v w : E), B (u + v) w = B u w + B v w) →
(∀ (c : ℝ) (u v : E), B (c • u) v = c * B u v) →
(∀ (u v : E), B u v = B v u) → (∀ (v : E), 0 ≤ B v v) → ∀ (u v : E), B u v ^ 2 ≤ B u u * B v vGPDYS.ne_zero_of_pos :
∀ {ι : Type u_1} [Nonempty ι] {z : ι → ℝ}, (∀ (i : ι), 0 < z i) → z ≠ 0GPDYS.Setting.inner_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner u v = ∑ i, P.w i * (u i * v i)GPDYS.Setting.inner_comm :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner u v = P.inner v uGPDYS.Setting.inner_add_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
P.inner (u + v) x = P.inner u x + P.inner v xGPDYS.Setting.inner_add_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
P.inner x (u + v) = P.inner x u + P.inner x vGPDYS.Setting.inner_smul_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (u v : ι → ℝ),
P.inner (c • u) v = c * P.inner u vGPDYS.Setting.inner_smul_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (u v : ι → ℝ),
P.inner u (c • v) = c * P.inner u vGPDYS.Setting.inner_neg_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner (-u) v = -P.inner u vGPDYS.Setting.inner_neg_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner u (-v) = -P.inner u vGPDYS.Setting.inner_sub_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
P.inner (u - v) x = P.inner u x - P.inner v xGPDYS.Setting.inner_sub_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
P.inner x (u - v) = P.inner x u - P.inner x vGPDYS.Setting.inner_zero_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.inner 0 v = 0GPDYS.Setting.inner_zero_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.inner v 0 = 0GPDYS.Setting.inner_sum_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {κ : Type u_2} (s : Finset κ)
(f : κ → ι → ℝ) (v : ι → ℝ), P.inner (∑ k ∈ s, f k) v = ∑ k ∈ s, P.inner (f k) vGPDYS.Setting.nrm2sq_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.nrm2sq v = P.inner v vGPDYS.Setting.nrm2sq_eq_sum :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.nrm2sq v = ∑ i, P.w i * v i ^ 2GPDYS.Setting.nrm2sq_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ P.nrm2sq vGPDYS.Setting.w_mul_sq_le_nrm2sq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ) (i : ι),
P.w i * v i ^ 2 ≤ P.nrm2sq vGPDYS.Setting.nrm2sq_eq_zero_iff :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.nrm2sq v = 0 ↔ v = 0GPDYS.Setting.nrm2sq_pos_of_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ}, v ≠ 0 → 0 < P.nrm2sq vGPDYS.Setting.nrm2_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.nrm2 v = √(P.nrm2sq v)GPDYS.Setting.nrm2_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ P.nrm2 vGPDYS.Setting.nrm2_sq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.nrm2 v ^ 2 = P.nrm2sq vGPDYS.Setting.nrm2_mul_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.nrm2 v * P.nrm2 v = P.nrm2sq vGPDYS.Setting.nrm2_pos_of_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ}, v ≠ 0 → 0 < P.nrm2 vGPDYS.Setting.nrm2_eq_zero_iff :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.nrm2 v = 0 ↔ v = 0GPDYS.Setting.nrm2sq_eq_one_of_nrm2 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ},
P.nrm2 v = 1 → P.nrm2sq v = 1GPDYS.Setting.nrm2_eq_one_of_nrm2sq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ},
P.nrm2sq v = 1 → P.nrm2 v = 1GPDYS.Setting.nrm2_eq_one_iff :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.nrm2 v = 1 ↔ P.nrm2sq v = 1GPDYS.Setting.nrm2sq_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (v : ι → ℝ),
P.nrm2sq (c • v) = c ^ 2 * P.nrm2sq vGPDYS.Setting.nrm2_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (v : ι → ℝ),
P.nrm2 (c • v) = |c| * P.nrm2 vGPDYS.Setting.nrm2sq_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.nrm2sq (u + v) = P.nrm2sq u + 2 * P.inner u v + P.nrm2sq vGPDYS.Setting.nrm2sq_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.nrm2sq (u - v) = P.nrm2sq u - 2 * P.inner u v + P.nrm2sq vGPDYS.Setting.nrm2sq_neg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.nrm2sq (-v) = P.nrm2sq v⟪u, v⟫_h² ≤ ‖u‖₂² ‖v‖₂².GPDYS.Setting.inner_sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner u v ^ 2 ≤ P.nrm2sq u * P.nrm2sq v⟪u, v⟫_h ≤ ‖u‖₂ ‖v‖₂.GPDYS.Setting.inner_le_nrm2_mul_nrm2 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner u v ≤ P.nrm2 u * P.nrm2 vGPDYS.Setting.abs_inner_le_nrm2_mul_nrm2 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
|P.inner u v| ≤ P.nrm2 u * P.nrm2 v‖·‖₂.GPDYS.Setting.nrm2_add_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.nrm2 (u + v) ≤ P.nrm2 u + P.nrm2 vGPDYS.Setting.nrm2_neg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.nrm2 (-v) = P.nrm2 vGPDYS.Setting.nrm2_sub_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.nrm2 (u - v) ≤ P.nrm2 u + P.nrm2 vGPDYS.Setting.nrm2_le_of_nrm2sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ} {c : ℝ},
0 ≤ c → P.nrm2sq v ≤ c ^ 2 → P.nrm2 v ≤ cGPDYS.Setting.nrm2_le_nrm2_iff :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.nrm2 u ≤ P.nrm2 v ↔ P.nrm2sq u ≤ P.nrm2sq v‖·‖₂ on nonnegative vectors.GPDYS.Setting.nrm2sq_le_nrm2sq_of_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {x y : ι → ℝ},
(∀ (i : ι), 0 ≤ x i) → (∀ (i : ι), x i ≤ y i) → P.nrm2sq x ≤ P.nrm2sq yGPDYS.Setting.nrm2_le_nrm2_of_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {x y : ι → ℝ},
(∀ (i : ι), 0 ≤ x i) → (∀ (i : ι), x i ≤ y i) → P.nrm2 x ≤ P.nrm2 yGPDYS.Setting.dotS_comm :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
u ⬝ᵥ P.S.mulVec v = v ⬝ᵥ P.S.mulVec uGPDYS.Setting.dotS_add_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
(u + v) ⬝ᵥ P.S.mulVec x = u ⬝ᵥ P.S.mulVec x + v ⬝ᵥ P.S.mulVec xGPDYS.Setting.dotS_add_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
x ⬝ᵥ P.S.mulVec (u + v) = x ⬝ᵥ P.S.mulVec u + x ⬝ᵥ P.S.mulVec vGPDYS.Setting.dotS_smul_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (u x : ι → ℝ),
c • u ⬝ᵥ P.S.mulVec x = c * u ⬝ᵥ P.S.mulVec xGPDYS.Setting.dotS_smul_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (u x : ι → ℝ),
x ⬝ᵥ P.S.mulVec (c • u) = c * x ⬝ᵥ P.S.mulVec uGPDYS.Setting.dotS_sub_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
(u - v) ⬝ᵥ P.S.mulVec x = u ⬝ᵥ P.S.mulVec x - v ⬝ᵥ P.S.mulVec xGPDYS.Setting.dotS_sub_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v x : ι → ℝ),
x ⬝ᵥ P.S.mulVec (u - v) = x ⬝ᵥ P.S.mulVec u - x ⬝ᵥ P.S.mulVec vGPDYS.Setting.dotS_neg_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u x : ι → ℝ),
-u ⬝ᵥ P.S.mulVec x = -(u ⬝ᵥ P.S.mulVec x)GPDYS.Setting.dotS_neg_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u x : ι → ℝ),
x ⬝ᵥ P.S.mulVec (-u) = -(x ⬝ᵥ P.S.mulVec u)GPDYS.Setting.dotS_zero_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (x : ι → ℝ), 0 ⬝ᵥ P.S.mulVec x = 0GPDYS.Setting.dotS_zero_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (x : ι → ℝ), x ⬝ᵥ P.S.mulVec 0 = 0GPDYS.Setting.kin_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.kin v = v ⬝ᵥ P.S.mulVec vGPDYS.Setting.kin_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ P.kin vGPDYS.Setting.kin_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (v : ι → ℝ),
P.kin (c • v) = c ^ 2 * P.kin vGPDYS.Setting.kin_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.kin (u + v) = P.kin u + 2 * u ⬝ᵥ P.S.mulVec v + P.kin vGPDYS.Setting.kin_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.kin (u - v) = P.kin u - 2 * u ⬝ᵥ P.S.mulVec v + P.kin vGPDYS.Setting.kin_neg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.kin (-v) = P.kin v(uᵀ S v)² ≤ (uᵀ S u)(vᵀ S v).GPDYS.Setting.dotS_sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
(u ⬝ᵥ P.S.mulVec v) ^ 2 ≤ P.kin u * P.kin vGPDYS.Setting.abs_dotS_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
|u ⬝ᵥ P.S.mulVec v| ≤ √(P.kin u) * √(P.kin v)GPDYS.Setting.negLap_apply :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ) (i : ι),
P.negLap v i = P.S.mulVec v i / P.w iGPDYS.Setting.inner_negLap :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner u (P.negLap v) = u ⬝ᵥ P.S.mulVec vGPDYS.Setting.inner_negLap_comm :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner u (P.negLap v) = P.inner (P.negLap u) vGPDYS.Setting.negLap_inner :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.inner (P.negLap u) v = u ⬝ᵥ P.S.mulVec vGPDYS.Setting.kin_eq_inner :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.kin v = P.inner v (P.negLap v)GPDYS.Setting.negLap_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.negLap (u + v) = P.negLap u + P.negLap vGPDYS.Setting.negLap_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (c : ℝ) (v : ι → ℝ),
P.negLap (c • v) = c • P.negLap vGPDYS.Setting.negLap_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u v : ι → ℝ),
P.negLap (u - v) = P.negLap u - P.negLap vGPDYS.Setting.negLap_neg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.negLap (-v) = -P.negLap vGPDYS.Setting.negLap_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι), P.negLap 0 = 0GPDYS.Setting.M_mulVec :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.M.mulVec v = fun i => P.w i * v iGPDYS.Setting.M_mulVec_negLap :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.M.mulVec (P.negLap v) = P.S.mulVec vGPDYS.Setting.pot_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ P.pot vGPDYS.Setting.wnorm4p4_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ GPDYS.wnorm4p4 P.w vGPDYS.Setting.wnorm6p6_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ GPDYS.wnorm6p6 P.w vGPDYS.Setting.wnorm3p3_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ GPDYS.wnorm3p3 P.w vGPDYS.Setting.H_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ P.H vGPDYS.Setting.energy_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.energy v = 1 / 2 * P.kin v + P.H vGPDYS.Setting.energy_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.energy v = 1 / 2 * P.kin v + 1 / 2 * P.pot v + P.β / 4 * GPDYS.wnorm4p4 P.w vGPDYS.Setting.energy_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ P.energy vGPDYS.Setting.kin_le_two_energy :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.kin v ≤ 2 * P.energy vGPDYS.Setting.quarter_wnorm4p4_le_energy :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.β / 4 * GPDYS.wnorm4p4 P.w v ≤ P.energy vGPDYS.Setting.nonlin_apply :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ) (i : ι),
P.nonlin v i = P.V i * v i + P.β * v i ^ 3GPDYS.Setting.inner_nonlin_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.inner (P.nonlin v) v = P.pot v + P.β * GPDYS.wnorm4p4 P.w vGPDYS.Setting.lam_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.lam v = P.kin v + P.pot v + P.β * GPDYS.wnorm4p4 P.w vGPDYS.Setting.lam_eq_energy :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.lam v = 2 * P.energy v + P.β / 2 * GPDYS.wnorm4p4 P.w vGPDYS.Setting.lam_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), 0 ≤ P.lam vGPDYS.Setting.lam_le_four_energy :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.lam v ≤ 4 * P.energy vGPDYS.Setting.gradE_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.gradE v = P.negLap v + P.nonlin vGPDYS.Setting.gradE_eq_lam_smul_add_g :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.gradE v = P.lam v • v + P.g vGPDYS.Setting.inner_gradE_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.inner (P.gradE v) v = P.lam vGPDYS.Setting.inner_g_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ},
P.nrm2sq v = 1 → P.inner (P.g v) v = 0GPDYS.Setting.inner_self_g :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ},
P.nrm2sq v = 1 → P.inner v (P.g v) = 0GPDYS.Setting.inner_gradE_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v d : ι → ℝ),
P.inner (P.gradE v) d = P.lam v * P.inner v d + P.inner (P.g v) d⟪n(u), d⟫_h expanded.GPDYS.Setting.inner_nonlin :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u d : ι → ℝ),
P.inner (P.nonlin u) d = ∑ i, P.w i * ((P.V i * u i + P.β * u i ^ 3) * d i)GPDYS.Setting.GX_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.GX γ v = v + γ • P.negLap vGPDYS.Setting.inner_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.inner u (P.GX γ v) = P.inner u v + γ * u ⬝ᵥ P.S.mulVec vGPDYS.Setting.GX_inner :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.inner (P.GX γ u) v = P.inner u v + γ * u ⬝ᵥ P.S.mulVec vGPDYS.Setting.inner_GX_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.inner v (P.GX γ v) = P.nrmGsq γ vGPDYS.Setting.GX_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.GX γ (u + v) = P.GX γ u + P.GX γ vGPDYS.Setting.GX_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.GX γ (u - v) = P.GX γ u - P.GX γ vGPDYS.Setting.GX_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ c : ℝ) (v : ι → ℝ),
P.GX γ (c • v) = c • P.GX γ vGPDYS.Setting.GX_neg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.GX γ (-v) = -P.GX γ vGPDYS.Setting.GX_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ), P.GX γ 0 = 0GPDYS.Setting.nrmGsq_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.nrmGsq γ v = P.nrm2sq v + γ * P.kin vGPDYS.Setting.nrmGsq_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), 0 ≤ P.nrmGsq γ vGPDYS.Setting.nrm2sq_le_nrmGsq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrm2sq v ≤ P.nrmGsq γ vGPDYS.Setting.mul_kin_le_nrmGsq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ} (v : ι → ℝ),
γ * P.kin v ≤ P.nrmGsq γ vGPDYS.Setting.nrmGsq_eq_zero_iff :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrmGsq γ v = 0 ↔ v = 0GPDYS.Setting.nrmGsq_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ c : ℝ) (v : ι → ℝ),
P.nrmGsq γ (c • v) = c ^ 2 * P.nrmGsq γ vGPDYS.Setting.nrmGsq_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.nrmGsq γ (u + v) = P.nrmGsq γ u + 2 * P.inner u (P.GX γ v) + P.nrmGsq γ v𝒢-inner product ⟪u, G_X v⟫_h.GPDYS.Setting.inner_GX_sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (u v : ι → ℝ), P.inner u (P.GX γ v) ^ 2 ≤ P.nrmGsq γ u * P.nrmGsq γ vGPDYS.Setting.normalize_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (z : ι → ℝ),
P.normalize z = (P.nrm2 z)⁻¹ • zGPDYS.Setting.nrm2_normalize :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 (P.normalize z) = 1GPDYS.Setting.nrm2sq_normalize :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2sq (P.normalize z) = 1GPDYS.Setting.nrm2_smul_normalize :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z • P.normalize z = zGPDYS.Setting.normalize_eq_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u : ι → ℝ},
P.nrm2 u = 1 → P.normalize u = uGPDYS.Setting.normalize_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (z : ι → ℝ) {c : ℝ},
0 < c → P.normalize (c • z) = P.normalize zGPDYS.Setting.normalize_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → (∀ (i : ι), 0 < z i) → ∀ (i : ι), 0 < P.normalize z iGPDYS.Setting.normalize_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
(∀ (i : ι), 0 ≤ z i) → ∀ (i : ι), 0 ≤ P.normalize z iGPDYS.Setting.iter_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u0 : ι → ℝ),
P.iter γ u0 0 = u0GPDYS.Setting.iter_succ :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u0 : ι → ℝ) (k : ℕ),
P.iter γ u0 (k + 1) = P.step γ (P.iter γ u0 k)GPDYS.Setting.uiter_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u0 : ι → ℝ) (k : ℕ),
P.uiter γ u0 k = P.normalize (P.iter γ u0 k)GPDYS.Setting.R_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (z : ι → ℝ),
P.R γ z = P.nrm2 z - 1 + γ * P.lam (P.normalize z)GPDYS.Setting.lyap_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (z : ι → ℝ),
P.lyap γ z = P.energy (P.normalize z) + P.R γ z ^ 2 / γGPDYS.Setting.energy_le_lyap :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 < γ → ∀ (z : ι → ℝ), P.energy (P.normalize z) ≤ P.lyap γ zGPDYS/Resolvent.lean — Section 3.2 (the resolvent and the X-norm)GPDYS.Setting.dot_M_mulVec :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (x y : ι → ℝ),
x ⬝ᵥ P.M.mulVec y = P.inner x yGPDYS.Setting.dot_MS_mulVec :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (x : ι → ℝ),
x ⬝ᵥ (P.M + γ • P.S).mulVec x = P.nrm2sq x + γ * P.kin xGPDYS.Setting.MS_mulVec_eq_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ {x : ι → ℝ}, (P.M + γ • P.S).mulVec x = 0 → x = 0GPDYS.Setting.MS_mulVec_injective :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → Function.Injective fun x => (P.M + γ • P.S).mulVec xGPDYS.Setting.MS_det_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → (P.M + γ • P.S).det ≠ 0GPDYS.Setting.MS_isUnit_det :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → IsUnit (P.M + γ • P.S).detGPDYS.Setting.M_mulVec_injective :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι),
Function.Injective fun x => P.M.mulVec xGPDYS.Setting.resolvent_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.resolvent γ v = (P.M + γ • P.S)⁻¹.mulVec (P.M.mulVec v)GPDYS.Setting.MS_mulVec_resolvent :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), (P.M + γ • P.S).mulVec (P.resolvent γ v) = P.M.mulVec vGPDYS.Setting.M_mulVec_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.M.mulVec (P.GX γ v) = (P.M + γ • P.S).mulVec vGPDYS.Setting.GX_resolvent :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.GX γ (P.resolvent γ v) = vGPDYS.Setting.resolvent_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.resolvent γ (P.GX γ v) = vGPDYS.Setting.GX_injective :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → Function.Injective (P.GX γ)GPDYS.Setting.GX_eq_iff :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v x : ι → ℝ), P.GX γ x = v ↔ x = P.resolvent γ vGPDYS.Setting.resolvent_zero_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ), P.resolvent 0 v = vGPDYS.Setting.resolvent_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.resolvent γ (u + v) = P.resolvent γ u + P.resolvent γ vGPDYS.Setting.resolvent_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.resolvent γ (u - v) = P.resolvent γ u - P.resolvent γ vGPDYS.Setting.resolvent_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ c : ℝ) (v : ι → ℝ),
P.resolvent γ (c • v) = c • P.resolvent γ vGPDYS.Setting.resolvent_neg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.resolvent γ (-v) = -P.resolvent γ vGPDYS.Setting.resolvent_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ), P.resolvent γ 0 = 0‖y + γ(-Δ_h y)‖₂² = ‖y‖₂² + 2γ ⟪y,-Δ_h y⟫_h + γ² ‖-Δ_h y‖₂².GPDYS.Setting.nrm2sq_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (y : ι → ℝ),
P.nrm2sq (P.GX γ y) = P.nrm2sq y + 2 * γ * P.kin y + γ ^ 2 * P.nrm2sq (P.negLap y)⟪y, -Δ_h(-Δ_h y)⟫_h = ‖-Δ_h y‖₂².GPDYS.Setting.dotS_negLap_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (y : ι → ℝ),
y ⬝ᵥ P.S.mulVec (P.negLap y) = P.nrm2sq (P.negLap y)⟪G_X y, -Δ_h G_X y⟫_h = ⟪y,-Δ_h y⟫_h + 2γ‖-Δ_h y‖₂² + γ² ⟪-Δ_h y, -Δ_h(-Δ_h y)⟫_h.GPDYS.Setting.kin_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (y : ι → ℝ),
P.kin (P.GX γ y) = P.kin y + 2 * γ * P.nrm2sq (P.negLap y) + γ ^ 2 * P.kin (P.negLap y)GPDYS.Setting.inner_GX_left_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (y : ι → ℝ),
P.inner (P.GX γ y) y = P.nrm2sq y + γ * P.kin yGPDYS.Setting.innerX_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v : ι → ℝ),
P.innerX γ u v = P.inner u (P.resolvent γ v)GPDYS.Setting.nrmXsq_def :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.nrmXsq γ v = P.inner v (P.resolvent γ v)‖v‖_X² = ‖y‖₂² + γ ⟪y,-Δ_h y⟫_h with y = G_X⁻¹ v.GPDYS.Setting.nrmXsq_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrmXsq γ v = P.nrm2sq (P.resolvent γ v) + γ * P.kin (P.resolvent γ v)G_X y for y = G_X⁻¹ v.GPDYS.Setting.exists_eq_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), ∃ y, P.GX γ y = v‖G_X v‖_X² = ‖v‖_𝒢², (3.7).GPDYS.Setting.nrmXsq_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrmXsq γ (P.GX γ v) = P.nrmGsq γ v⟪u, G_X v⟫_X = ⟪u, v⟫_h.GPDYS.Setting.innerX_GX_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (u v : ι → ℝ), P.innerX γ u (P.GX γ v) = P.inner u vh-self-adjointness of the resolvent: ⟪u, G_X⁻¹ v⟫_h = ⟪G_X⁻¹ u, v⟫_h.GPDYS.Setting.innerX_comm :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (u v : ι → ℝ), P.innerX γ u v = P.innerX γ v uGPDYS.Setting.innerX_add_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v x : ι → ℝ),
P.innerX γ (u + v) x = P.innerX γ u x + P.innerX γ v xGPDYS.Setting.innerX_add_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v x : ι → ℝ),
P.innerX γ x (u + v) = P.innerX γ x u + P.innerX γ x vGPDYS.Setting.innerX_smul_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ c : ℝ) (u x : ι → ℝ),
P.innerX γ (c • u) x = c * P.innerX γ u xGPDYS.Setting.innerX_smul_right :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ c : ℝ) (u x : ι → ℝ),
P.innerX γ x (c • u) = c * P.innerX γ x uGPDYS.Setting.innerX_sub_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u v x : ι → ℝ),
P.innerX γ (u - v) x = P.innerX γ u x - P.innerX γ v xGPDYS.Setting.innerX_neg_left :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (u x : ι → ℝ),
P.innerX γ (-u) x = -P.innerX γ u xGPDYS.Setting.nrmXsq_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), 0 ≤ P.nrmXsq γ vGPDYS.Setting.nrmXsq_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ c : ℝ) (v : ι → ℝ),
P.nrmXsq γ (c • v) = c ^ 2 * P.nrmXsq γ vGPDYS.Setting.nrmXsq_neg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (v : ι → ℝ),
P.nrmXsq γ (-v) = P.nrmXsq γ vX: ⟪u, v⟫_X² ≤ ‖u‖_X² ‖v‖_X².GPDYS.Setting.innerX_sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (u v : ι → ℝ), P.innerX γ u v ^ 2 ≤ P.nrmXsq γ u * P.nrmXsq γ v‖·‖_X.GPDYS.Setting.sqrt_nrmXsq_add_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (u v : ι → ℝ), √(P.nrmXsq γ (u + v)) ≤ √(P.nrmXsq γ u) + √(P.nrmXsq γ v)‖v‖_X² ≤ ‖v‖₂², (3.5).GPDYS.Setting.nrmXsq_le_nrm2sq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrmXsq γ v ≤ P.nrm2sq v‖v‖_X > 0 for v ≠ 0, (3.5).GPDYS.Setting.nrmXsq_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ {v : ι → ℝ}, v ≠ 0 → 0 < P.nrmXsq γ v‖G_X⁻¹ v‖₂² ≤ ‖v‖_X², (3.5).GPDYS.Setting.nrm2sq_resolvent_le_nrmXsq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrm2sq (P.resolvent γ v) ≤ P.nrmXsq γ v‖v‖₂² - ‖v‖_X² ≤ γ ⟪v, -Δ_h v⟫_h.
The lower bound is nrmXsq_le_nrm2sq.GPDYS.Setting.nrm2sq_sub_nrmXsq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrm2sq v - P.nrmXsq γ v ≤ γ * P.kin v‖v‖_X² ≤ ‖v‖_𝒢².GPDYS.Setting.nrmXsq_le_nrmGsq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (v : ι → ℝ), P.nrmXsq γ v ≤ P.nrmGsq γ v-1 ≤ a ≤ 0, the operator a I + (1 - a) G_X⁻¹ is a contraction in ‖·‖₂.GPDYS.Setting.nrm2sq_contraction :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ a : ℝ},
0 ≤ γ → -1 ≤ a → a ≤ 0 → ∀ (u : ι → ℝ), P.nrm2sq (a • u + (1 - a) • P.resolvent γ u) ≤ P.nrm2sq u‖-Δ_h y‖₂² ≤ μ ⟪y,-Δ_h y⟫_h if ⟪·,-Δ_h ·⟫_h ≤ μ ‖·‖₂².GPDYS.Setting.nrm2sq_negLap_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {μ : ℝ},
0 ≤ μ → (∀ (x : ι → ℝ), P.kin x ≤ μ * P.nrm2sq x) → ∀ (y : ι → ℝ), P.nrm2sq (P.negLap y) ≤ μ * P.kin y‖v‖₂² ≤ (1 + γ μ) ‖v‖_X² if ⟪·,-Δ_h ·⟫_h ≤ μ ‖·‖₂², (5.3).GPDYS.Setting.nrm2sq_le_mul_nrmXsq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ μ : ℝ},
0 ≤ γ → 0 ≤ μ → (∀ (x : ι → ℝ), P.kin x ≤ μ * P.nrm2sq x) → ∀ (v : ι → ℝ), P.nrm2sq v ≤ (1 + γ * μ) * P.nrmXsq γ vGPDYS.Setting.resolvent_apply :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (b : ι → ℝ) (i : ι),
P.resolvent γ b i = ∑ j, (P.M + γ • P.S)⁻¹ i j * (P.w j * b j)GPDYS.Setting.resolvent_pos_of_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 < γ → ∀ {b : ι → ℝ}, (∀ (i : ι), 0 ≤ b i) → b ≠ 0 → ∀ (i : ι), 0 < P.resolvent γ b iGPDYS.Setting.resolvent_nonneg_of_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ {b : ι → ℝ}, (∀ (i : ι), 0 ≤ b i) → ∀ (i : ι), 0 ≤ P.resolvent γ b iGPDYS/Holder.lean — Hölder inequalities used in Lemma 4.3‖v‖₆⁶ ≥ 0 for nonnegative weights.GPDYS.wnorm6p6_nonneg' :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ), (∀ (i : ι), 0 ≤ w i) → ∀ (v : ι → ℝ), 0 ≤ GPDYS.wnorm6p6 w v‖v‖₃³ ≥ 0 for nonnegative weights.GPDYS.wnorm3p3_nonneg' :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ), (∀ (i : ι), 0 ≤ w i) → ∀ (v : ι → ℝ), 0 ≤ GPDYS.wnorm3p3 w v‖v‖₆ ≥ 0 for nonnegative weights.GPDYS.wnorm6_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ), (∀ (i : ι), 0 ≤ w i) → ∀ (v : ι → ℝ), 0 ≤ GPDYS.wnorm6 w v‖v‖₃ ≥ 0 for nonnegative weights.GPDYS.wnorm3_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ), (∀ (i : ι), 0 ≤ w i) → ∀ (v : ι → ℝ), 0 ≤ GPDYS.wnorm3 w v‖v‖₆⁶ = ∑ᵢ wᵢ vᵢ⁶ for nonnegative weights.GPDYS.wnorm6_pow_six :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ (v : ι → ℝ), GPDYS.wnorm6 w v ^ 6 = GPDYS.wnorm6p6 w v‖v‖₃³ = ∑ᵢ wᵢ |vᵢ|³ for nonnegative weights.GPDYS.wnorm3_pow_three :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ (v : ι → ℝ), GPDYS.wnorm3 w v ^ 3 = GPDYS.wnorm3p3 w v‖v²‖₃ = ‖v‖₆² (componentwise square).GPDYS.wnorm3_sq_eq :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ (v : ι → ℝ), (GPDYS.wnorm3 w fun i => v i ^ 2) = GPDYS.wnorm6 w v ^ 23 and 3/2: ∑ᵢ wᵢ aᵢ² bᵢ² ≤ ‖a‖₆² ‖b‖₃².GPDYS.holder_six_three :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ (a b : ι → ℝ), ∑ i, w i * (a i ^ 2 * b i ^ 2) ≤ GPDYS.wnorm6 w a ^ 2 * GPDYS.wnorm3 w b ^ 24/3 and 4: ‖b‖₃² ≤ ‖b‖₂ ‖b‖₆.GPDYS.wnorm3_sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ (b : ι → ℝ), GPDYS.wnorm3 w b ^ 2 ≤ GPDYS.wnorm2 w b * GPDYS.wnorm6 w b∑ᵢ wᵢ |uᵢ|³ |cᵢ|³ ≤ ‖u‖₆³ ‖c‖₆³.GPDYS.holder_cubes :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) →
∀ (u c : ι → ℝ), ∑ i, w i * (|u i| ^ 3 * |c i| ^ 3) ≤ GPDYS.wnorm6 w u ^ 3 * GPDYS.wnorm6 w c ^ 3‖·‖₆ under a componentwise bound |aᵢ| ≤ |bᵢ|.GPDYS.wnorm6_le_of_abs_le :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ {a b : ι → ℝ}, (∀ (i : ι), |a i| ≤ |b i|) → GPDYS.wnorm6 w a ≤ GPDYS.wnorm6 w b|w^{1/6} x|⁶ = w x⁶ for w ≥ 0 (the integrand of the Minkowski inequality).GPDYS.abs_rpow_sixth_mul_pow_six :
∀ (w : ℝ), 0 ≤ w → ∀ (x : ℝ), |w ^ (1 / 6) * x| ^ 6 = w * x ^ 6‖·‖₆ triangle inequality (Minkowski), used for ‖u + σδ‖₆ ≤ (1-σ)‖u‖₆ + σ‖u⁺‖₆.GPDYS.wnorm6_add_le :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ (a b : ι → ℝ), GPDYS.wnorm6 w (a + b) ≤ GPDYS.wnorm6 w a + GPDYS.wnorm6 w b‖c • v‖₆ = |c| ‖v‖₆.GPDYS.wnorm6_smul :
∀ {ι : Type u_1} [inst : Fintype ι] (w : ι → ℝ),
(∀ (i : ι), 0 ≤ w i) → ∀ (c : ℝ) (v : ι → ℝ), GPDYS.wnorm6 w (c • v) = |c| * GPDYS.wnorm6 w vGPDYS/SobolevConst.lean — a Sobolev constant exists on every fixed nonempty meshw
and positive semidefinite S. The proof chooses (∑ᵢ wᵢ)^{1/6} / √(minᵢ wᵢ).GPDYS.exists_sobolev_const :
∀ {ι : Type u_1} [inst : Fintype ι] [Nonempty ι] (w : ι → ℝ),
(∀ (i : ι), 0 < w i) →
∀ (S : Matrix ι ι ℝ),
(∀ (v : ι → ℝ), 0 ≤ v ⬝ᵥ S.mulVec v) →
∃ CS, 0 < CS ∧ ∀ (v : ι → ℝ), GPDYS.wnorm6 w v ≤ CS * √(v ⬝ᵥ S.mulVec v + GPDYS.wnorm2sq w v)GPDYS/Constants.lean — Section 3.3: Lemma 3.1 and Lemma 3.2GPDYS.Setting.wmin_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (i : ι), P.wmin ≤ P.w iGPDYS.Setting.wmin_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι], 0 < P.wminGPDYS.Setting.le_Vinf :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (i : ι), P.V i ≤ P.VinfGPDYS.Setting.Vinf_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι], 0 ≤ P.VinfSᵢᵢ ≥ 0, as the value of the quadratic form of S at the ith unit vector.GPDYS.Setting.S_diag_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (i : ι), 0 ≤ P.S i iGPDYS.Setting.le_Λd :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (i : ι), P.S i i / P.w i ≤ P.ΛdGPDYS.Setting.Λd_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι], 0 ≤ P.Λd⟪V v, v⟫_h ≤ ‖V‖_∞ ‖v‖₂².GPDYS.Setting.pot_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.pot v ≤ P.Vinf * P.nrm2sq v‖V v‖₂ ≤ ‖V‖_∞ ‖v‖₂.GPDYS.Setting.nrm2_Vmul_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
(P.nrm2 fun i => P.V i * v i) ≤ P.Vinf * P.nrm2 vGPDYS.Setting.energy_le_E0 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ), P.energy u0 ≤ P.E0 u0GPDYS.Setting.E0_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ),
P.E0 u0 ≤ 9 / 8 * P.energy u0GPDYS.Setting.energy_pos_of_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ}, v ≠ 0 → 0 < P.energy vGPDYS.Setting.E0_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ), u0 ≠ 0 → 0 < P.E0 u0GPDYS.Setting.E0_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ), 0 ≤ P.E0 u0GPDYS.Setting.P0_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ), 0 ≤ P.P0 u01).GPDYS.Setting.CS_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι], 0 < P.CSGPDYS.Setting.P0_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
0 < P.P0 u0GPDYS.Setting.U0_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
0 ≤ P.U0 u0GPDYS.Setting.U0_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
u0 ≠ 0 → 0 < P.U0 u0GPDYS.Setting.U0_le_inv_wmin :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ), P.U0 u0 ≤ 1 / P.wminGPDYS.Setting.B0_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
0 ≤ P.B0 u0GPDYS.Setting.E0_le_D :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
P.E0 u0 ≤ P.D u0GPDYS.Setting.B0_le_D :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ), P.B0 u0 ≤ P.D u0GPDYS.Setting.D_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
u0 ≠ 0 → 0 < P.D u0GPDYS.Setting.B1_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
u0 ≠ 0 → 0 < P.B1 u0GPDYS.Setting.C0_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
0 < P.C0 u0GPDYS.Setting.L0_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
u0 ≠ 0 → 0 < P.L0 u0GPDYS.Setting.γmax_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
u0 ≠ 0 → 0 < P.γmax u0s = √(B₁² + 12 D Λ_d),
4 (γ B₁ + 3 γ² D Λ_d - 1) = (γ (B₁ + s) - 2) (γ (s - B₁) + 2).GPDYS.Setting.C4_identity :
∀ {B D Λ γ s : ℝ},
s ^ 2 = B ^ 2 + 12 * D * Λ → 4 * (γ * B + 3 * γ ^ 2 * D * Λ - 1) = (γ * (B + s) - 2) * (γ * (s - B) + 2)γ ≤ γ_max implies (C1)–(C4).GPDYS.Setting.conditions_of_le_γmax :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
u0 ≠ 0 → ∀ {γ : ℝ}, 0 < γ → γ ≤ P.γmax u0 → P.Conditions u0 γγ ≤ γ_max.GPDYS.Setting.le_γmax_of_conditions :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
u0 ≠ 0 → ∀ {γ : ℝ}, 0 < γ → P.Conditions u0 γ → γ ≤ P.γmax u0γ ≤ 1 / max{1, 128 E_h(u⁰)}.GPDYS.Setting.le_inv_max_of_conditions :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι] {γ : ℝ},
0 < γ → P.Conditions u0 γ → γ ≤ 1 / max 1 (128 * P.energy u0)𝓛(z⁰) ≤ E₀ for z⁰ = u⁰ ∈ 𝓜.
The proof uses 𝓛(z⁰) = E_h(u⁰) + γ λ(u⁰)².GPDYS.Setting.lyap_init_le_E0 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u0 : ι → ℝ) [Nonempty ι],
P.nrm2 u0 = 1 → ∀ {γ : ℝ}, 0 < γ → P.Conditions u0 γ → P.lyap γ u0 ≤ P.E0 u0GPDYS.Setting.nonempty_of_nrm2sq_eq_one :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ},
P.nrm2sq v = 1 → Nonempty ι⟪v, -Δ_h v⟫_h ≤ 2E₀.GPDYS.Setting.kin_le_two_E0 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → P.kin v ≤ 2 * P.E0 u0‖v‖²_{1,h} ≤ 2E₀ + 1.GPDYS.Setting.h1norm_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → P.kin v + P.nrm2sq v ≤ 2 * P.E0 u0 + 1‖v‖₆² ≤ P₀.GPDYS.Setting.wnorm6_sq_le_P0 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → GPDYS.wnorm6 P.w v ^ 2 ≤ P.P0 u0‖v‖₆⁶ ≤ P₀³.GPDYS.Setting.wnorm6p6_le_P0_cube :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → GPDYS.wnorm6p6 P.w v ≤ P.P0 u0 ^ 3vᵢ² ≤ U₀ for every i (i.e. ‖v‖_∞² ≤ U₀).GPDYS.Setting.sq_le_U0 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → ∀ (i : ι), v i ^ 2 ≤ P.U0 u0‖v³‖₂ ≤ min{P₀^{3/2}, U₀}.GPDYS.Setting.nrm2_cube_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → (P.nrm2 fun i => v i ^ 3) ≤ min (P.P0 u0 ^ (3 / 2)) (P.U0 u0)‖v‖₄⁴ ≤ min{P₀^{3/2}, U₀}.GPDYS.Setting.wnorm4p4_le_min :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → GPDYS.wnorm4p4 P.w v ≤ min (P.P0 u0 ^ (3 / 2)) (P.U0 u0)‖n(v)‖₂ ≤ B₀.GPDYS.Setting.nrm2_nonlin_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → ∀ [Nonempty ι], P.nrm2 (P.nonlin v) ≤ P.B0 u0⟪n(v), v⟫_h ≤ B₀.GPDYS.Setting.inner_nonlin_self_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → ∀ [Nonempty ι], P.inner (P.nonlin v) v ≤ P.B0 u0λ(v) ≤ 2D; lam_nonneg gives the lower bound.GPDYS.Setting.lam_le_two_D :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 v : ι → ℝ},
P.nrm2sq v = 1 → P.energy v ≤ P.E0 u0 → ∀ [Nonempty ι], P.lam v ≤ 2 * P.D u0GPDYS/Step.lean — Section 4.1: Lemma 4.1 and Lemma 4.2δ = u⁺ - u of one step.def delta (γ : ℝ) (z : ι → ℝ) : ι → ℝ := P.normalize (P.step γ z) - P.normalize zGPDYS.Setting.delta :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ι → ℝ𝒯(u, d) = H(u + d) - H(u) - ⟪n(u), d⟫_h of the explicit part of the
energy, (4.2).def taylorT (u d : ι → ℝ) : ℝ := P.H (u + d) - P.H u - P.inner (P.nonlin u) dGPDYS.Setting.taylorT :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → (ι → ℝ) → ℝ⟪u, u⁺ - u⟫_h = -½ ‖u⁺ - u‖₂² for unit vectors u, u⁺.GPDYS.Setting.inner_sub_self_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u up : ι → ℝ},
P.nrm2sq u = 1 → P.nrm2sq up = 1 → P.inner u (up - u) = -(1 / 2) * P.nrm2sq (up - u)‖u⁺ - u‖₂² = 2 (1 - ⟪u, u⁺⟫_h) for unit vectors u, u⁺.GPDYS.Setting.nrm2sq_sub_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u up : ι → ℝ},
P.nrm2sq u = 1 → P.nrm2sq up = 1 → P.nrm2sq (up - u) = 2 * (1 - P.inner u up)‖δ‖₂² = 2 (1 - ⟪u, z⁺⟫_h / ‖z⁺‖₂), the second form in (4.1).GPDYS.Setting.nrm2sq_delta_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ} {z : ι → ℝ},
z ≠ 0 → P.step γ z ≠ 0 → P.nrm2sq (P.delta γ z) = 2 * (1 - P.inner (P.normalize z) (P.step γ z) / P.nrm2 (P.step γ z))𝒯(u, d) = ½ ∑ᵢ wᵢ Vᵢ dᵢ² + (β/2) ∑ᵢ wᵢ dᵢ² (3uᵢ² + 2uᵢdᵢ + ½dᵢ²).GPDYS.Setting.taylorT_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u d : ι → ℝ),
P.taylorT u d =
1 / 2 * ∑ i, P.w i * (P.V i * d i ^ 2) +
P.β / 2 * ∑ i, P.w i * (d i ^ 2 * (3 * u i ^ 2 + 2 * u i * d i + d i ^ 2 / 2))E_h(u + d) - E_h(u) = ⟪∇E_h(u), d⟫_h + ½ ⟪d, -Δ_h d⟫_h + 𝒯(u, d).GPDYS.Setting.taylorE :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (u d : ι → ℝ),
P.energy (u + d) - P.energy u = P.inner (P.gradE u) d + 1 / 2 * P.kin d + P.taylorT u dG_X z = ‖z‖₂ u + ‖z‖₂ γ (-Δ_h u) for z ≠ 0 and u = z/‖z‖₂.GPDYS.Setting.GX_eq_nrm2_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) {z : ι → ℝ},
z ≠ 0 → P.GX γ z = P.nrm2 z • P.normalize z + (P.nrm2 z * γ) • P.negLap (P.normalize z)z = c • u substituted: for any scalar c and vector u,
G_X (c u + G_X⁻¹(2u - c u - γ n(u)) - u) = u - γ n(u) - γ (1 - c) (-Δ_h u).GPDYS.Setting.GX_step_aux :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ →
∀ (c : ℝ) (u : ι → ℝ),
P.GX γ (c • u + P.resolvent γ (2 • u - c • u - γ • P.nonlin u) - u) =
u - γ • P.nonlin u - (γ * (1 - c)) • P.negLap uG_X z⁺ = u - γ n(u) - γ(1 - ‖z‖₂)(-Δ_h u).GPDYS.Setting.GX_step :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ →
∀ {z : ι → ℝ},
z ≠ 0 →
P.GX γ (P.step γ z) =
P.normalize z - γ • P.nonlin (P.normalize z) - (γ * (1 - P.nrm2 z)) • P.negLap (P.normalize z)G_X (z⁺ - z) = (1 - ‖z‖₂) u - γ ∇E_h(u).GPDYS.Setting.GX_step_sub_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ {z : ι → ℝ}, z ≠ 0 → P.GX γ (P.step γ z - z) = (1 - P.nrm2 z) • P.normalize z - γ • P.gradE (P.normalize z)G_X (z⁺ - z) = -(R u + γ g(u)).GPDYS.Setting.GX_step_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ {z : ι → ℝ}, z ≠ 0 → P.GX γ (P.step γ z - z) = -(P.R γ z • P.normalize z + γ • P.g (P.normalize z))z⁺ - z = ‖z⁺‖₂ δ + (‖z⁺‖₂ - ‖z‖₂) u.GPDYS.Setting.step_sub_decomp :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ →
∀ {z : ι → ℝ},
z ≠ 0 →
P.step γ z ≠ 0 →
P.step γ z - z = P.nrm2 (P.step γ z) • P.delta γ z + (P.nrm2 (P.step γ z) - P.nrm2 z) • P.normalize z‖z⁺‖₂ G_X δ = (1 - ‖z⁺‖₂) u - γ ∇E_h(u) - γ(‖z⁺‖₂ - ‖z‖₂)(-Δ_h u).GPDYS.Setting.GX_delta :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ →
∀ {z : ι → ℝ},
z ≠ 0 →
P.step γ z ≠ 0 →
P.nrm2 (P.step γ z) • P.GX γ (P.delta γ z) =
(1 - P.nrm2 (P.step γ z)) • P.normalize z - γ • P.gradE (P.normalize z) -
(γ * (P.nrm2 (P.step γ z) - P.nrm2 z)) • P.negLap (P.normalize z)(1 + γ⟪u,-Δ_h u⟫_h)(‖z⁺‖₂ - ‖z‖₂) = -R - ‖z⁺‖₂ (γ⟪-Δ_h u, δ⟫_h - ½‖δ‖₂²).GPDYS.Setting.radial_identity :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ →
∀ {z : ι → ℝ},
z ≠ 0 →
P.step γ z ≠ 0 →
(1 + γ * P.kin (P.normalize z)) * (P.nrm2 (P.step γ z) - P.nrm2 z) =
-P.R γ z -
P.nrm2 (P.step γ z) * (γ * P.normalize z ⬝ᵥ P.S.mulVec (P.delta γ z) - 1 / 2 * P.nrm2sq (P.delta γ z))γ(E_h(u) - E_h(u⁺)) = ((‖z⁺‖₂+1)/2)‖δ‖₂² + γ(‖z⁺‖₂ - ½)⟪δ,-Δ_h δ⟫_h
+ γ(‖z⁺‖₂ - ‖z‖₂)⟪-Δ_h u, δ⟫_h - γ 𝒯(u, δ).GPDYS.Setting.energy_identity :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ →
∀ {z : ι → ℝ},
z ≠ 0 →
P.step γ z ≠ 0 →
γ * (P.energy (P.normalize z) - P.energy (P.normalize (P.step γ z))) =
(P.nrm2 (P.step γ z) + 1) / 2 * P.nrm2sq (P.delta γ z) +
γ * (P.nrm2 (P.step γ z) - 1 / 2) * P.kin (P.delta γ z) +
γ * (P.nrm2 (P.step γ z) - P.nrm2 z) * P.normalize z ⬝ᵥ P.S.mulVec (P.delta γ z) -
γ * P.taylorT (P.normalize z) (P.delta γ z)R⁺ = -½‖δ‖₂² - γ(‖z⁺‖₂ - ‖z‖₂)⟪-Δ_h u, u⁺⟫_h - γ(‖z⁺‖₂ - 1)⟪-Δ_h δ, u⁺⟫_h
+ γ⟪n(u⁺) - n(u), u⁺⟫_h.GPDYS.Setting.residual_identity :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ →
∀ {z : ι → ℝ},
z ≠ 0 →
P.step γ z ≠ 0 →
P.R γ (P.step γ z) =
-(1 / 2) * P.nrm2sq (P.delta γ z) -
γ * (P.nrm2 (P.step γ z) - P.nrm2 z) * P.normalize z ⬝ᵥ P.S.mulVec (P.normalize (P.step γ z)) -
γ * (P.nrm2 (P.step γ z) - 1) * P.delta γ z ⬝ᵥ P.S.mulVec (P.normalize (P.step γ z)) +
γ * P.inner (P.nonlin (P.normalize (P.step γ z)) - P.nonlin (P.normalize z)) (P.normalize (P.step γ z))GPDYS/Nonlinear.lean — Section 4.2: Lemma 4.30 ≤ x ≤ y and an arbitrary real C₀
(no sign condition on C₀ is needed):
C₀ x y ≤ (C₀ + 2 max{C₀ - 1/4, 0}²) x² + (y² - x²)/8.GPDYS.Setting.sobolev_quadratic_bound_aux :
∀ (C0 : ℝ) {x y : ℝ}, 0 ≤ x → x ≤ y → C0 * x * y ≤ (C0 + 2 * max (C0 - 1 / 4) 0 ^ 2) * x ^ 2 + (y ^ 2 - x ^ 2) / 8𝒯(u, δ) ≤ ½ (‖V‖_∞ + 3β U₀) ‖δ‖₂².GPDYS.Setting.taylorT_le_pointwise :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 u up : ι → ℝ},
P.nrm2sq u = 1 →
P.nrm2sq up = 1 →
P.energy u ≤ P.E0 u0 →
P.energy up ≤ P.E0 u0 →
∀ [Nonempty ι], P.taylorT u (up - u) ≤ 1 / 2 * (P.Vinf + 3 * P.β * P.U0 u0) * P.nrm2sq (up - u)𝒯(u, δ) ≤ ½ (‖V‖_∞ ‖δ‖₂² + C₀ ‖δ‖₂ ‖δ‖_{1,h}), with ‖δ‖_{1,h} = √(⟪δ,-Δ_h δ⟫_h + ‖δ‖₂²).GPDYS.Setting.taylorT_le_sobolev :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 u up : ι → ℝ},
P.nrm2sq u = 1 →
P.nrm2sq up = 1 →
P.energy u ≤ P.E0 u0 →
P.energy up ≤ P.E0 u0 →
∀ [Nonempty ι],
P.taylorT u (up - u) ≤
1 / 2 * (P.Vinf * P.nrm2sq (up - u) + P.C0 u0 * P.nrm2 (up - u) * √(P.kin (up - u) + P.nrm2sq (up - u)))γ 𝒯(u, δ) ≤ (1/16) ‖δ‖_𝒢² under (C3).GPDYS.Setting.taylorT_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 u up : ι → ℝ},
P.nrm2sq u = 1 →
P.nrm2sq up = 1 →
P.energy u ≤ P.E0 u0 →
P.energy up ≤ P.E0 u0 →
∀ [Nonempty ι] {γ : ℝ}, 0 ≤ γ → γ * P.L0 u0 ≤ 1 / 8 → γ * P.taylorT u (up - u) ≤ 1 / 16 * P.nrmGsq γ (up - u)‖a b²‖₂ ≤ min{P₀^{3/2}, U₀} for unit vectors a, b of energy at most E₀
(here applied to the pairs (u, u⁺), (u⁺, u) and (u⁺, u⁺)).GPDYS.Setting.nrm2_mixed_cube_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 u up : ι → ℝ},
P.nrm2sq u = 1 →
P.nrm2sq up = 1 →
P.energy u ≤ P.E0 u0 →
P.energy up ≤ P.E0 u0 → ∀ [Nonempty ι], (P.nrm2 fun i => u i * up i ^ 2) ≤ min (P.P0 u0 ^ (3 / 2)) (P.U0 u0)|⟪n(u⁺) - n(u), u⁺⟫_h| ≤ 3 B₀ ‖δ‖₂.GPDYS.Setting.abs_inner_nonlin_sub_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 u up : ι → ℝ},
P.nrm2sq u = 1 →
P.nrm2sq up = 1 →
P.energy u ≤ P.E0 u0 →
P.energy up ≤ P.E0 u0 → ∀ [Nonempty ι], |P.inner (P.nonlin up - P.nonlin u) up| ≤ 3 * P.B0 u0 * P.nrm2 (up - u)0 ≤ x ≤ y,
C₀ x y ≤ (C₀ + 2 max{C₀ - 1/4, 0}²) x² + (y² - x²)/8.GPDYS.Setting.sobolev_quadratic_bound :
∀ (C0 : ℝ),
0 ≤ C0 → ∀ {x y : ℝ}, 0 ≤ x → x ≤ y → C0 * x * y ≤ (C0 + 2 * max (C0 - 1 / 4) 0 ^ 2) * x ^ 2 + (y ^ 2 - x ^ 2) / 8GPDYS/Positivity.lean — Section 4.3: Lemma 4.4nᵢ(u) ≤ B₁ uᵢ for u > 0 with E_h(u) ≤ E₀.GPDYS.Setting.nonlin_le_B1_mul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 u : ι → ℝ},
P.nrm2sq u = 1 → P.energy u ≤ P.E0 u0 → (∀ (i : ι), 0 < u i) → ∀ (i : ι), P.nonlin u i ≤ P.B1 u0 * u i(-Δ_h u)ᵢ ≤ Λ_d uᵢ for u > 0.GPDYS.Setting.negLap_le_Λd_mul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u : ι → ℝ},
(∀ (i : ι), 0 < u i) → ∀ (i : ι), P.negLap u i ≤ P.Λd * u in(u) ≥ 0 for u ≥ 0.GPDYS.Setting.nonlin_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u : ι → ℝ},
(∀ (i : ι), 0 ≤ u i) → ∀ (i : ι), 0 ≤ P.nonlin u iz⁺ = (‖z‖₂ - 1) u + (2 - ‖z‖₂) G_X⁻¹ u - γ G_X⁻¹ n(u).GPDYS.Setting.step_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ} {z : ι → ℝ},
z ≠ 0 →
P.step γ z =
(P.nrm2 z - 1) • P.normalize z + (2 - P.nrm2 z) • P.resolvent γ (P.normalize z) -
γ • P.resolvent γ (P.nonlin (P.normalize z))G_X z⁺ ≥ 0 componentwise, by (C4).GPDYS.Setting.GX_step_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → ∀ (i : ι), 0 ≤ P.GX γ (P.step γ z) iG_X z⁺ ≠ 0, by (C2).GPDYS.Setting.GX_step_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → P.GX γ (P.step γ z) ≠ 0z⁺ > 0 componentwise.GPDYS.Setting.step_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → ∀ (i : ι), 0 < P.step γ z iGPDYS.Setting.step_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 → 1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → P.step γ z ≠ 0‖z⁺‖₂ ≤ 1.GPDYS.Setting.nrm2_step_le_one :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → P.nrm2 (P.step γ z) ≤ 11 - ⟪u, z⁺⟫_h = (2 - ‖z‖₂)(1 - ‖u‖_X²) + γ ⟪G_X⁻¹ u, n(u)⟫_h.GPDYS.Setting.one_sub_inner_step_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
1 - P.inner (P.normalize z) (P.step γ z) =
(2 - P.nrm2 z) * (1 - P.nrmXsq γ (P.normalize z)) +
γ * P.inner (P.resolvent γ (P.normalize z)) (P.nonlin (P.normalize z))0 ≤ 1 - ⟪u, z⁺⟫_h.GPDYS.Setting.one_sub_inner_step_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → 0 ≤ 1 - P.inner (P.normalize z) (P.step γ z)1 - ⟪u, z⁺⟫_h ≤ 3γD.GPDYS.Setting.one_sub_inner_step_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → 1 - P.inner (P.normalize z) (P.step γ z) ≤ 3 * γ * P.D u0⟪u, z⁺⟫_h ≤ ‖z⁺‖₂.GPDYS.Setting.inner_step_le_nrm2 :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.inner (P.normalize z) (P.step γ z) ≤ P.nrm2 (P.step γ z)1 - 3γD ≤ ‖z⁺‖₂.GPDYS.Setting.nrm2_step_ge :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → 1 - 3 * γ * P.D u0 ≤ P.nrm2 (P.step γ z)‖δ‖₂² ≤ 2 (1 - ⟪u, z⁺⟫_h).GPDYS.Setting.nrm2sq_delta_le_two_mul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.nrm2sq (P.delta γ z) ≤ 2 * (1 - P.inner (P.normalize z) (P.step γ z))‖δ‖₂² ≤ 6γD.GPDYS.Setting.nrm2sq_delta_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → P.nrm2sq (P.delta γ z) ≤ 6 * γ * P.D u0|R| ≤ 3γD.GPDYS.Setting.abs_R_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → |P.R γ z| ≤ 3 * γ * P.D u0GPDYS/Descent.lean — Section 4.4: Lemma 4.5 and Lemma 4.6C₁ = ‖V‖_∞ + 3β/w_min.def C1 : ℝ := P.Vinf + 3 * P.β / P.wminGPDYS.Setting.C1 :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ𝒯(u, u⁺ - u) ≤ ½ C₁ ‖u⁺ - u‖₂², using only vᵢ² ≤ 1/w_min for ‖v‖₂ = 1.GPDYS.Setting.taylorT_le_crude :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u up : ι → ℝ},
P.nrm2sq u = 1 → P.nrm2sq up = 1 → P.taylorT u (up - u) ≤ 1 / 2 * P.C1 * P.nrm2sq (up - u)γ |xᵀ S y| ≤ √(γ xᵀ S x) √(γ yᵀ S y) for γ ≥ 0.GPDYS.Setting.mul_abs_dotS_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (x y : ι → ℝ), γ * |x ⬝ᵥ P.S.mulVec y| ≤ √(γ * P.kin x) * √(γ * P.kin y)𝒢-inner product: ⟪x, G_X y⟫_h = ⟪G_X x, y⟫_h.GPDYS.Setting.inner_GX_symm :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (x y : ι → ℝ),
P.inner x (P.GX γ y) = P.inner (P.GX γ x) yd - (⟪u, G_X d⟫_h / ‖u‖_𝒢²) u is 𝒢-orthogonal to u.GPDYS.Setting.inner_GX_perp :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) {u : ι → ℝ},
P.nrmGsq γ u ≠ 0 → ∀ (d : ι → ℝ), P.inner u (P.GX γ (d - (P.inner u (P.GX γ d) / P.nrmGsq γ u) • u)) = 0GPDYS.Setting.perp_inner_GX :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) {u : ι → ℝ},
P.nrmGsq γ u ≠ 0 → ∀ (d : ι → ℝ), P.inner (d - (P.inner u (P.GX γ d) / P.nrmGsq γ u) • u) (P.GX γ u) = 0𝒢-orthogonal decomposition of d along u.GPDYS.Setting.nrmGsq_eq_perp_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) {u : ι → ℝ},
P.nrmGsq γ u ≠ 0 →
∀ (d : ι → ℝ),
P.nrmGsq γ d =
P.nrmGsq γ (d - (P.inner u (P.GX γ d) / P.nrmGsq γ u) • u) +
(P.inner u (P.GX γ d) / P.nrmGsq γ u) ^ 2 * P.nrmGsq γ u‖a - b‖_X².GPDYS.Setting.nrmXsq_sub_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ (a b : ι → ℝ), P.nrmXsq γ (a - b) = P.nrmXsq γ a - 2 * P.innerX γ a b + P.nrmXsq γ b‖a - b‖_𝒢².GPDYS.Setting.nrmGsq_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (a b : ι → ℝ),
P.nrmGsq γ (a - b) = P.nrmGsq γ a - 2 * P.inner a (P.GX γ b) + P.nrmGsq γ bγ|⟪-Δ_h u, δ⟫_h| ≤ √(2γD) ‖δ‖_𝒢.GPDYS.Setting.abs_dotS_u_delta_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
γ * |P.normalize z ⬝ᵥ P.S.mulVec (P.delta γ z)| ≤ √(2 * γ * P.D u0) * √(P.nrmGsq γ (P.delta γ z))½‖δ‖₂² ≤ √(3γD/2) ‖δ‖_𝒢, from ‖δ‖₂² ≤ 6γD and ‖δ‖₂ ≤ ‖δ‖_𝒢.GPDYS.Setting.half_nrm2sq_delta_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → 1 / 2 * P.nrm2sq (P.delta γ z) ≤ √(3 / 2) * √(γ * P.D u0) * √(P.nrmGsq γ (P.delta γ z))|‖z⁺‖₂ - ‖z‖₂| ≤ |R| + (8/3) √(γD) ‖δ‖_𝒢.GPDYS.Setting.abs_nrm2_step_sub_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
|P.nrm2 (P.step γ z) - P.nrm2 z| ≤ |P.R γ z| + 8 / 3 * √(γ * P.D u0) * √(P.nrmGsq γ (P.delta γ z))γ(28D + 2C₁) ≤ 1 then
E_h(u⁺) ≤ E_h(u) + 2D R².GPDYS.Setting.energy_step_le_of_small :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
γ * (28 * P.D u0 + 2 * P.C1) ≤ 1 →
P.energy (P.normalize (P.step γ z)) ≤ P.energy (P.normalize z) + 2 * P.D u0 * P.R γ z ^ 2γ(E_h(u) - E_h(u⁺)) ≥ (7/16 - 10γD)‖δ‖_𝒢² - (1/5)R².GPDYS.Setting.energy_drop :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.energy (P.normalize (P.step γ z)) ≤ P.E0 u0 →
γ * (P.energy (P.normalize z) - P.energy (P.normalize (P.step γ z))) ≥
(7 / 16 - 10 * γ * P.D u0) * P.nrmGsq γ (P.delta γ z) - 1 / 5 * P.R γ z ^ 2(R⁺)² ≤ 8γ²D² R² + (128/25) γD ‖δ‖_𝒢².GPDYS.Setting.residual_sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.energy (P.normalize (P.step γ z)) ≤ P.E0 u0 →
P.R γ (P.step γ z) ^ 2 ≤
8 * γ ^ 2 * P.D u0 ^ 2 * P.R γ z ^ 2 + 128 / 25 * γ * P.D u0 * P.nrmGsq γ (P.delta γ z)γ(𝓛(z) - 𝓛(z⁺)) ≥ (5/16)‖δ‖_𝒢² + (3/4)R².GPDYS.Setting.conditional_descent :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.energy (P.normalize (P.step γ z)) ≤ P.E0 u0 →
γ * (P.lyap γ z - P.lyap γ (P.step γ z)) ≥
5 / 16 * P.nrmGsq γ (P.delta γ z) + 3 / 4 * P.R γ z ^ 2δ = 0 and R = 0 then g(u) = 0 and z⁺ = z.
(For γ = 0 one has z⁺ = u and δ = 0 for every z, so γ > 0 is needed for g(u) = 0.)GPDYS.Setting.descent_equality_case :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 < γ →
∀ {z : ι → ℝ}, z ≠ 0 → P.step γ z ≠ 0 → P.delta γ z = 0 → P.R γ z = 0 → P.g (P.normalize z) = 0 ∧ P.step γ z = zR = 0 and g(u) = 0 then z⁺ = z (used in the barrier argument).GPDYS.Setting.step_eq_self_of_R_g :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {γ : ℝ},
0 ≤ γ → ∀ {z : ι → ℝ}, z ≠ 0 → P.R γ z = 0 → P.g (P.normalize z) = 0 → P.step γ z = z‖u‖_𝒢² (‖z⁺‖₂ - ‖z‖₂) = -R - ‖z⁺‖₂ ⟪u, G_X δ⟫_h.GPDYS.Setting.nrmGsq_mul_nrm2_sub :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.nrmGsq γ (P.normalize z) * (P.nrm2 (P.step γ z) - P.nrm2 z) =
-P.R γ z - P.nrm2 (P.step γ z) * P.inner (P.normalize z) (P.GX γ (P.delta γ z))z⁺ - z = ‖z⁺‖₂ δ⊥ - (R/‖u‖_𝒢²) u, where
δ⊥ = δ - (⟪u, G_X δ⟫_h/‖u‖_𝒢²) u is the 𝒢-orthogonal part of δ.GPDYS.Setting.step_sub_eq_perp :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.step γ z - z =
P.nrm2 (P.step γ z) •
(P.delta γ z -
(P.inner (P.normalize z) (P.GX γ (P.delta γ z)) / P.nrmGsq γ (P.normalize z)) •
P.normalize z) -
(P.R γ z / P.nrmGsq γ (P.normalize z)) • P.normalize zγ²‖g(u)‖_X² ≤ (5/4)‖δ‖_𝒢² + 10γD R².GPDYS.Setting.gradX_sq_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
γ ^ 2 * P.nrmXsq γ (P.g (P.normalize z)) ≤
5 / 4 * P.nrmGsq γ (P.delta γ z) + 10 * γ * P.D u0 * P.R γ z ^ 2‖z⁺ - z‖_𝒢² ≤ ‖δ‖_𝒢² + R².GPDYS.Setting.nrmGsq_step_sub_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ} {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
P.energy (P.normalize z) ≤ P.E0 u0 →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.nrmGsq γ (P.step γ z - z) ≤ P.nrmGsq γ (P.delta γ z) + P.R γ z ^ 2GPDYS/Barrier.lean — Section 4.5: Lemma 4.7 (energy barrier)z_θ = (1 - θ(1 - ‖z‖₂)) u, (4.27).def zcont (z : ι → ℝ) (θ : ℝ) : ι → ℝ := (1 - θ * (1 - P.nrm2 z)) • P.normalize zGPDYS.Setting.zcont :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝ → ι → ℝθγ from z_θ, (4.29).def stepcont (γ : ℝ) (z : ι → ℝ) (θ : ℝ) : ι → ℝ := P.step (θ * γ) (P.zcont z θ)GPDYS.Setting.stepcont :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℝ → ι → ℝφ(θ) = E_h(u_θ⁺).def φcont (γ : ℝ) (z : ι → ℝ) (θ : ℝ) : ℝ := P.energy (P.normalize (P.stepcont γ z θ))GPDYS.Setting.φcont :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝ → (ι → ℝ) → ℝ → ℝ‖z_θ‖₂ = 1 - θ(1 - ‖z‖₂) for θ ∈ [0,1], (4.28).GPDYS.Setting.nrm2_zcont :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ {θ : ℝ}, 0 ≤ θ → θ ≤ 1 → P.nrm2 (P.zcont z θ) = 1 - θ * (1 - P.nrm2 z)1 - θ(1 - ‖z‖₂) > 0 for θ ∈ [0,1] and z ≠ 0.GPDYS.Setting.zcont_coeff_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ {θ : ℝ}, θ ≤ 1 → 0 < 1 - θ * (1 - P.nrm2 z)GPDYS.Setting.zcont_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ {θ : ℝ}, 0 ≤ θ → θ ≤ 1 → P.zcont z θ ≠ 0z_θ is u.GPDYS.Setting.normalize_zcont :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ {θ : ℝ}, 0 ≤ θ → θ ≤ 1 → P.normalize (P.zcont z θ) = P.normalize zz_1 = z.GPDYS.Setting.zcont_one :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → P.zcont z 1 = zz_0⁺ = u (a step of size 0 from u returns u).GPDYS.Setting.stepcont_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ (γ : ℝ), P.stepcont γ z 0 = P.normalize zz_1⁺ = z⁺.GPDYS.Setting.stepcont_one :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ (γ : ℝ), P.stepcont γ z 1 = P.step γ zR_{θγ}(z_θ) = θ R(z), (4.30).GPDYS.Setting.R_zcont :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ (γ : ℝ) {θ : ℝ}, 0 ≤ θ → θ ≤ 1 → P.R (θ * γ) (P.zcont z θ) = θ * P.R γ z𝓛_{θγ}(z_θ) = E_h(u) + θ R²/γ, (4.30).GPDYS.Setting.lyap_zcont :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 →
P.nrm2 z ≤ 1 →
∀ {γ : ℝ},
0 < γ → ∀ {θ : ℝ}, 0 < θ → θ ≤ 1 → P.lyap (θ * γ) (P.zcont z θ) = P.energy (P.normalize z) + θ * P.R γ z ^ 2 / γz_θ⁺ on [0,1]:
z_θ⁺ = z_θ - u + G_{θγ}⁻¹ (2u - z_θ - θγ n(u)).GPDYS.Setting.stepcont_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 →
P.nrm2 z ≤ 1 →
∀ (γ : ℝ) {θ : ℝ},
0 ≤ θ →
θ ≤ 1 →
P.stepcont γ z θ =
P.zcont z θ - P.normalize z +
P.resolvent (θ * γ) (2 • P.normalize z - P.zcont z θ - (θ * γ) • P.nonlin (P.normalize z))θ ↦ (M + θγS)⁻¹ is continuous on [0,1]
(for γ ≥ 0), since det (M + θγ S) ≠ 0 there.GPDYS.Setting.continuousOn_inv_MS :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ {γ : ℝ}, 0 ≤ γ → ContinuousOn (fun θ => (P.M + (θ * γ) • P.S)⁻¹) (Set.Icc 0 1)θ ↦ z_θ⁺ is continuous on [0,1].GPDYS.Setting.stepcont_continuousOn :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → P.nrm2 z ≤ 1 → ∀ {γ : ℝ}, 0 ≤ γ → ContinuousOn (P.stepcont γ z) (Set.Icc 0 1)E_h is a continuous function on ι → ℝ.GPDYS.Setting.energy_continuous :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι), Continuous P.energyg is a continuous function on ι → ℝ.GPDYS.Setting.g_continuous :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι), Continuous P.g‖·‖₂ is continuous.GPDYS.Setting.nrm2_continuous :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι), Continuous P.nrm2normalize is continuous at every nonzero vector.GPDYS.Setting.normalize_continuousAt :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {z : ι → ℝ},
z ≠ 0 → ContinuousAt P.normalize zθ ∈ (0,1], (C2)–(C4) hold for θγ,
and 1 - 3θγD ≤ ‖z_θ‖₂ ≤ 1. Positivity and the energy bound are proved separately.GPDYS.Setting.zcont_hyp :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 →
∀ {θ : ℝ},
0 < θ →
θ ≤ 1 →
θ * γ * P.D u0 ≤ 1 / 128 ∧
θ * γ * P.L0 u0 ≤ 1 / 8 ∧
θ * γ * P.B1 u0 + 3 * (θ * γ) ^ 2 * P.D u0 * P.Λd ≤ 1 ∧
1 - 3 * (θ * γ) * P.D u0 ≤ P.nrm2 (P.zcont z θ) ∧ P.nrm2 (P.zcont z θ) ≤ 1E_h(u) ≤ E₀.GPDYS.Setting.energy_normalize_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → P.energy (P.normalize z) ≤ P.E0 u0z_θ⁺ ≠ 0 for every θ ∈ [0,1].GPDYS.Setting.stepcont_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → ∀ {θ : ℝ}, 0 ≤ θ → θ ≤ 1 → P.stepcont γ z θ ≠ 0φ is continuous on [0,1].GPDYS.Setting.φcont_continuousOn :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → ContinuousOn (P.φcont γ z) (Set.Icc 0 1)φ(0) ≤ E₀, using the identity φ(0) = E_h(u).GPDYS.Setting.φcont_zero_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → P.φcont γ z 0 ≤ P.E0 u0C₁ > 0.GPDYS.Setting.C1_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → 0 < P.C1θ, φ(θ) ≤ E₀: the threshold θ₁ = min{1, 1/(γ(28D + 2C₁))} > 0 works.GPDYS.Setting.φcont_le_of_small :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 →
∀ {θ : ℝ}, 0 ≤ θ → θ ≤ min 1 (1 / (γ * (28 * P.D u0 + 2 * P.C1))) → P.φcont γ z θ ≤ P.E0 u0φ(θ) ≤ E₀ for some θ ∈ (0,1], then
φ(θ) ≤ E_h(u) + θ R²/(4γ) - (5/(16 θγ)) ‖δ_θ‖_𝒢², by the conditional descent.GPDYS.Setting.φcont_le_of_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 →
∀ {θ : ℝ},
0 < θ →
θ ≤ 1 →
P.φcont γ z θ ≤ P.E0 u0 →
P.φcont γ z θ ≤
P.energy (P.normalize z) + θ * P.R γ z ^ 2 / (4 * γ) -
5 / (16 * (θ * γ)) * P.nrmGsq (θ * γ) (P.delta (θ * γ) (P.zcont z θ))φ(θ) ≤ E₀ for some θ ∈ (0,1] and not (R = 0 and g(u) = 0),
then φ(θ) < E₀.GPDYS.Setting.φcont_lt_of_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 →
∀ {θ : ℝ},
0 < θ →
θ ≤ 1 →
P.φcont γ z θ ≤ P.E0 u0 →
¬(P.R γ z = 0 ∧ P.g (P.normalize z) = 0) → P.φcont γ z θ < P.E0 u0R = 0 and g(u) = 0, then φ(θ) = E_h(u) for every θ ∈ [0,1].
The proof first uses step_eq_self_of_R_g to show z_θ⁺ = z_θ.GPDYS.Setting.φcont_eq_of_R_g :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 →
P.R γ z = 0 →
P.g (P.normalize z) = 0 →
∀ {θ : ℝ}, 0 ≤ θ → θ ≤ 1 → P.φcont γ z θ = P.energy (P.normalize z)E_h(u⁺) ≤ E₀.GPDYS.Setting.energy_barrier :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ * P.D u0 ≤ 1 / 128 →
γ * P.L0 u0 ≤ 1 / 8 →
γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → P.energy (P.normalize (P.step γ z)) ≤ P.E0 u0GPDYS/OneStep.lean — Section 4.5: Proposition 4.8GPDYS.Setting.onestep_conditions :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ → γ ≤ P.γmax u0 → γ * P.D u0 ≤ 1 / 128 ∧ γ * P.L0 u0 ≤ 1 / 8 ∧ γ * P.B1 u0 + 3 * γ ^ 2 * P.D u0 * P.Λd ≤ 1E_h(u) ≤ E₀.GPDYS.Setting.onestep_energy_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u0 : ι → ℝ} {γ : ℝ},
0 < γ → ∀ {z : ι → ℝ}, P.lyap γ z ≤ P.E0 u0 → P.energy (P.normalize z) ≤ P.E0 u0z⁺.GPDYS.Setting.onestep_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z → P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → ∀ (i : ι), 0 < P.step γ z iz⁺.GPDYS.Setting.onestep_radial :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 → 1 - 3 * γ * P.D u0 ≤ P.nrm2 (P.step γ z) ∧ P.nrm2 (P.step γ z) ≤ 1E_h(u⁺) ≤ E₀, by the energy barrier.GPDYS.Setting.onestep_energy :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 → P.lyap γ z ≤ P.E0 u0 → P.energy (P.normalize (P.step γ z)) ≤ P.E0 u0𝓛(z) - 𝓛(z⁺) ≥ ¼ γ ‖g(u)‖_X² + R²/(2γ).GPDYS.Setting.onestep_drop :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 →
P.lyap γ z - P.lyap γ (P.step γ z) ≥
1 / 4 * γ * P.nrmXsq γ (P.g (P.normalize z)) + P.R γ z ^ 2 / (2 * γ)𝓛(z) - 𝓛(z⁺) ≥ (5/(16γ)) ‖z⁺ - z‖_𝒢².GPDYS.Setting.onestep_drop' :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
u0 ≠ 0 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {z : ι → ℝ},
z ≠ 0 →
(∀ (i : ι), 0 < P.normalize z i) →
1 - 3 * γ * P.D u0 ≤ P.nrm2 z →
P.nrm2 z ≤ 1 →
P.lyap γ z ≤ P.E0 u0 →
P.lyap γ z - P.lyap γ (P.step γ z) ≥ 5 / (16 * γ) * P.nrmGsq γ (P.step γ z - z)GPDYS/GroundState.lean — Remark 2.3 / Appendix A (the discrete ground state)vᵀ S v written as a double sum.GPDYS.Setting.kin_eq_double_sum :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.kin v = ∑ i, ∑ j, P.S i j * (v i * v j)u > 0 componentwise and any v,
∑ᵢ (vᵢ²/uᵢ) (S u)ᵢ ≤ vᵀ S v.GPDYS.Setting.picone :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u : ι → ℝ},
(∀ (i : ι), 0 < u i) → ∀ (v : ι → ℝ), ∑ i, v i ^ 2 / u i * P.S.mulVec u i ≤ P.kin v|v|ᵀ S |v| ≤ vᵀ S v, since the off-diagonal entries of S are nonpositive.GPDYS.Setting.kin_abs_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
(P.kin fun i => |v i|) ≤ P.kin vE_h(|v|) ≤ E_h(v).GPDYS.Setting.energy_abs_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
(P.energy fun i => |v i|) ≤ P.energy v‖ |v| ‖₂² = ‖v‖₂².GPDYS.Setting.nrm2sq_abs :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
(P.nrm2sq fun i => |v i|) = P.nrm2sq v-Δ_h v = λ(v) v - n(v).GPDYS.Setting.negLap_eq_of_critical :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ},
P.g v = 0 → P.negLap v = P.lam v • v - P.nonlin vE_h on 𝓜 is strictly positive.GPDYS.Setting.critical_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {v : ι → ℝ},
P.nrm2sq v = 1 → (∀ (i : ι), 0 ≤ v i) → P.g v = 0 → ∀ (i : ι), 0 < v iu ∈ 𝓜 and any nonnegative v ∈ 𝓜,
E_h(v) ≥ E_h(u) + (β/4) ∑ᵢ wᵢ (vᵢ² - uᵢ²)².GPDYS.Setting.energy_ge_of_critical :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u v : ι → ℝ},
P.nrm2sq u = 1 →
(∀ (i : ι), 0 < u i) →
P.g u = 0 →
P.nrm2sq v = 1 → (∀ (i : ι), 0 ≤ v i) → P.energy u + P.β / 4 * ∑ i, P.w i * (v i ^ 2 - u i ^ 2) ^ 2 ≤ P.energy vE_h on 𝓜.GPDYS.Setting.energy_le_of_critical :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u v : ι → ℝ},
P.nrm2sq u = 1 → (∀ (i : ι), 0 < u i) → P.g u = 0 → P.nrm2sq v = 1 → P.energy u ≤ P.energy vv ∈ 𝓜 with E_h(v) ≤ E_h(u),
where u > 0 is a critical point, equals u.GPDYS.Setting.eq_of_nonneg_le_energy :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u v : ι → ℝ},
P.nrm2sq u = 1 →
(∀ (i : ι), 0 < u i) → P.g u = 0 → P.nrm2sq v = 1 → (∀ (i : ι), 0 ≤ v i) → P.energy v ≤ P.energy u → v = u𝓜
coincide.GPDYS.Setting.eq_of_critical_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u v : ι → ℝ},
P.nrm2sq u = 1 → (∀ (i : ι), 0 ≤ u i) → P.g u = 0 → P.nrm2sq v = 1 → (∀ (i : ι), 0 ≤ v i) → P.g v = 0 → v = uGPDYS/Main.lean — Section 5: Theorem 3.4f ^ 2 → 0 then f → 0.GPDYS.tendsto_zero_of_sq_tendsto_zero :
∀ {α : Type u_1} {l : Filter α} {f : α → ℝ}, Filter.Tendsto (fun x => f x ^ 2) l (nhds 0) → Filter.Tendsto f l (nhds 0)c * f → 0 with c ≠ 0 then f → 0.GPDYS.tendsto_zero_of_const_mul_tendsto_zero :
∀ {α : Type u_1} {l : Filter α} {f : α → ℝ} {c : ℝ},
c ≠ 0 → Filter.Tendsto (fun x => c * f x) l (nhds 0) → Filter.Tendsto f l (nhds 0)‖·‖₂² is continuous.GPDYS.Setting.nrm2sq_continuous :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι), Continuous P.nrm2sqvᵀ S v as a double sum.GPDYS.Setting.kin_eq_sum_sum :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (v : ι → ℝ),
P.kin v = ∑ i, ∑ j, P.S i j * (v i * v j)μ ≥ 0 with
⟪v, -Δ_h v⟫_h ≤ μ ‖v‖₂² for all v (in the paper, μ_max is the largest eigenvalue).GPDYS.Setting.exists_kin_bound :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
∃ μ, 0 ≤ μ ∧ ∀ (v : ι → ℝ), P.kin v ≤ μ * P.nrm2sq v𝓜 is compact.GPDYS.Setting.sphere_isCompact :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
IsCompact {v | P.nrm2sq v = 1}k,
u^k > 0, 1 - 3γD ≤ ‖z^k‖₂ ≤ 1 and 𝓛^k ≤ E₀.GPDYS.Setting.invariant :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ (k : ℕ),
(∀ (i : ι), 0 < P.uiter γ u0 k i) ∧
1 - 3 * γ * P.D u0 ≤ P.nrm2 (P.iter γ u0 k) ∧
P.nrm2 (P.iter γ u0 k) ≤ 1 ∧ P.lyap γ (P.iter γ u0 k) ≤ P.E0 u0GPDYS.Setting.iter_ne_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) → P.nrm2 u0 = 1 → ∀ {γ : ℝ}, 0 < γ → γ ≤ P.γmax u0 → ∀ (k : ℕ), P.iter γ u0 k ≠ 0𝓛^k - 𝓛^{k+1} ≥ ¼γ‖g(u^k)‖_X² + (R^k)²/(2γ).GPDYS.Setting.drop :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ (k : ℕ),
P.lyap γ (P.iter γ u0 k) - P.lyap γ (P.iter γ u0 (k + 1)) ≥
1 / 4 * γ * P.nrmXsq γ (P.g (P.uiter γ u0 k)) + P.R γ (P.iter γ u0 k) ^ 2 / (2 * γ)∑_{k < m} (¼γ‖g^k‖_X² + (R^k)²/(2γ)) is at most 𝓛⁰.GPDYS.Setting.sum_drop_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ (m : ℕ),
∑ k ∈ Finset.range m,
(1 / 4 * γ * P.nrmXsq γ (P.g (P.uiter γ u0 k)) + P.R γ (P.iter γ u0 k) ^ 2 / (2 * γ)) ≤
P.lyap γ u0¼γ‖g^k‖_X² + (R^k)²/(2γ) are summable.GPDYS.Setting.drop_summable :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
Summable fun k => 1 / 4 * γ * P.nrmXsq γ (P.g (P.uiter γ u0 k)) + P.R γ (P.iter γ u0 k) ^ 2 / (2 * γ)‖g(u^k)‖_X² → 0.GPDYS.Setting.nrmXsq_g_tendsto_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ → γ ≤ P.γmax u0 → Filter.Tendsto (fun k => P.nrmXsq γ (P.g (P.uiter γ u0 k))) Filter.atTop (nhds 0)R^k → 0.GPDYS.Setting.R_tendsto_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ}, 0 < γ → γ ≤ P.γmax u0 → Filter.Tendsto (fun k => P.R γ (P.iter γ u0 k)) Filter.atTop (nhds 0)g(u^k) → 0.GPDYS.Setting.g_tendsto_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ}, 0 < γ → γ ≤ P.γmax u0 → Filter.Tendsto (fun k => P.g (P.uiter γ u0 k)) Filter.atTop (nhds 0)(u^k)
is a nonnegative critical point of E_h on 𝓜.GPDYS.Setting.accumulation_point_critical :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {ns : ℕ → ℕ},
Filter.Tendsto ns Filter.atTop Filter.atTop →
∀ {ustar : ι → ℝ},
Filter.Tendsto (fun j => P.uiter γ u0 (ns j)) Filter.atTop (nhds ustar) →
P.nrm2sq ustar = 1 ∧ (∀ (i : ι), 0 ≤ ustar i) ∧ P.g ustar = 0𝓜.GPDYS.Setting.uiter_mem_sphere :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 → ∀ {γ : ℝ}, 0 < γ → γ ≤ P.γmax u0 → ∀ (k : ℕ), P.uiter γ u0 k ∈ {v | P.nrm2sq v = 1}GPDYS.Setting.exists_accumulation_point :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∃ ustar ns, StrictMono ns ∧ Filter.Tendsto (fun j => P.uiter γ u0 (ns j)) Filter.atTop (nhds ustar)u⁰ and a step
size 0 < γ ≤ γ_max, the iterates u^k = z^k/‖z^k‖₂ of (DYS I) are positive for every k,
and converge to the discrete ground state u_GS, the unique positive global minimizer of E_h
on 𝓜, which is also the unique nonnegative critical point of E_h|_𝓜; moreover
E_h(u^k) → E_h(u_GS) = min_𝓜 E_h.GPDYS.Setting.main_theorem :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
(∀ (k : ℕ) (i : ι), 0 < P.uiter γ u0 k i) ∧
∃ uGS,
(∀ (i : ι), 0 < uGS i) ∧
P.nrm2 uGS = 1 ∧
P.g uGS = 0 ∧
(∀ (v : ι → ℝ), P.nrm2 v = 1 → P.energy uGS ≤ P.energy v) ∧
(∀ (v : ι → ℝ), P.nrm2 v = 1 → (∀ (i : ι), 0 ≤ v i) → P.energy v ≤ P.energy uGS → v = uGS) ∧
(∀ (v : ι → ℝ), P.nrm2 v = 1 → (∀ (i : ι), 0 ≤ v i) → P.g v = 0 → v = uGS) ∧
Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds uGS) ∧
Filter.Tendsto (fun k => P.energy (P.uiter γ u0 k)) Filter.atTop (nhds (P.energy uGS))u_GS ∈ 𝓜 which
is a critical point of E_h|_𝓜, the global minimizer of E_h on 𝓜, and the unique
nonnegative critical point. It is obtained from Theorem 3.4 as the limit of the iteration
started from the normalized constant vector with the step size γ_max.GPDYS.Setting.exists_groundState :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
∃ uGS,
(∀ (i : ι), 0 < uGS i) ∧
P.nrm2 uGS = 1 ∧
P.g uGS = 0 ∧
(∀ (v : ι → ℝ), P.nrm2 v = 1 → P.energy uGS ≤ P.energy v) ∧
∀ (v : ι → ℝ), P.nrm2 v = 1 → (∀ (i : ι), 0 ≤ v i) → P.g v = 0 → v = uGSGPDYS/Rate.lean — Section 5: Theorem 5.1m_GS = minᵢ pᵢ on a nonempty mesh; the empty-index value is zero.def mGS {ι : Type*} [Fintype ι] (p : ι → ℝ) : ℝ := ⨅ i, p iGPDYS.mGS :
{ι : Type u_1} → [Fintype ι] → (ι → ℝ) → ℝη = min{γν/(4(1+γμ)), 1/2}, (5.5).def η (γ μ ν : ℝ) : ℝ := min (γ * ν / (4 * (1 + γ * μ))) (1 / 2)GPDYS.η :
ℝ → ℝ → ℝ → ℝℋ = -Δ_h + n'(p) - λ(p) I of (5.4), applied to w.def hess (p w : ι → ℝ) : ι → ℝ := P.negLap w + P.nonlin' p w - P.lam p • wGPDYS.Setting.hess :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → (ι → ℝ) → ι → ℝ⟪w, ℋ w⟫_h.def hessForm (p w : ι → ℝ) : ℝ := P.inner w (P.hess p w)GPDYS.Setting.hessForm :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → (ι → ℝ) → ℝ⟪w, ℋ w⟫_h over unit tangent vectors.
For a positive critical point and 2 ≤ Fintype.card ι, exists_unit_tangent and
bddBelow_nu_set justify the infimum used in the rate theorem. Attainment as a minimum
is proved by nu_attained in Spectral.lean. The empty-set value is zero.def nu (p : ι → ℝ) : ℝ :=
sInf {x : ℝ | ∃ w : ι → ℝ, P.nrm2sq w = 1 ∧ P.inner p w = 0 ∧ x = P.hessForm p w}GPDYS.Setting.nu :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → ℝGPDYS.Setting.hessForm_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p w : ι → ℝ),
P.hessForm p w = P.kin w + P.pot w + 3 * P.β * ∑ i, P.w i * (p i ^ 2 * w i ^ 2) - P.lam p * P.nrm2sq w⟪w, A_p w⟫_h ≥ λ(p) ‖w‖₂² for every w, where A_p = -Δ_h + V + β diag(p²).GPDYS.Setting.rayleigh_of_critical :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 → ∀ (w : ι → ℝ), P.lam p * P.nrm2sq w ≤ P.kin w + P.pot w + P.β * ∑ i, P.w i * (p i ^ 2 * w i ^ 2)GPDYS.Setting.mGS_le :
∀ {ι : Type u_1} [inst : Fintype ι] (p : ι → ℝ) (i : ι), GPDYS.mGS p ≤ p iGPDYS.Setting.mGS_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [Nonempty ι] {p : ι → ℝ}, (∀ (i : ι), 0 < p i) → 0 < GPDYS.mGS p⟪w, ℋ w⟫_h ≥ 2β m_GS² ‖w‖₂² for every w.GPDYS.Setting.hessForm_ge :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) → P.g p = 0 → ∀ (w : ι → ℝ), 2 * P.β * GPDYS.mGS p ^ 2 * P.nrm2sq w ≤ P.hessForm p wN ≥ 2 there is a unit vector orthogonal to p.GPDYS.Setting.exists_unit_tangent :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι),
2 ≤ Fintype.card ι → ∀ {p : ι → ℝ}, (∀ (i : ι), 0 < p i) → ∃ w, P.nrm2sq w = 1 ∧ P.inner p w = 0ν ≥ 2β m_GS².GPDYS.Setting.nu_ge :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι),
2 ≤ Fintype.card ι →
∀ {p : ι → ℝ}, P.nrm2sq p = 1 → (∀ (i : ι), 0 < p i) → P.g p = 0 → 2 * P.β * GPDYS.mGS p ^ 2 ≤ P.nu pν > 0.GPDYS.Setting.nu_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι),
2 ≤ Fintype.card ι → ∀ {p : ι → ℝ}, P.nrm2sq p = 1 → (∀ (i : ι), 0 < p i) → P.g p = 0 → 0 < P.nu pn'(p) is linear in its second argument.GPDYS.Setting.nonlin'_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p u v : ι → ℝ),
P.nonlin' p (u + v) = P.nonlin' p u + P.nonlin' p vGPDYS.Setting.nonlin'_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p : ι → ℝ) (c : ℝ) (v : ι → ℝ),
P.nonlin' p (c • v) = c • P.nonlin' p vn'(p) is a diagonal operator, hence h-self-adjoint.GPDYS.Setting.inner_nonlin'_comm :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p x y : ι → ℝ),
P.inner x (P.nonlin' p y) = P.inner (P.nonlin' p x) yℋ is linear.GPDYS.Setting.hess_add :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p u v : ι → ℝ),
P.hess p (u + v) = P.hess p u + P.hess p vGPDYS.Setting.hess_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p : ι → ℝ) (c : ℝ) (v : ι → ℝ),
P.hess p (c • v) = c • P.hess p vGPDYS.Setting.hess_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p : ι → ℝ), P.hess p 0 = 0ℋ is h-self-adjoint: ⟪x, ℋ y⟫_h = ⟪ℋ x, y⟫_h.GPDYS.Setting.inner_hess_comm :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p x y : ι → ℝ),
P.inner x (P.hess p y) = P.inner (P.hess p x) yGPDYS.Setting.hessForm_smul :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p : ι → ℝ) (c : ℝ) (w : ι → ℝ),
P.hessForm p (c • w) = c ^ 2 * P.hessForm p wGPDYS.Setting.hessForm_zero :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p : ι → ℝ), P.hessForm p 0 = 0ν is bounded below by 2β m_GS².GPDYS.Setting.bddBelow_nu_set :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) → P.g p = 0 → BddBelow {x | ∃ w, P.nrm2sq w = 1 ∧ P.inner p w = 0 ∧ x = P.hessForm p w}⟪w, ℋ w⟫_h ≥ ν ‖w‖₂² for every tangent vector w (⟪p, w⟫_h = 0).GPDYS.Setting.hessForm_ge_nu :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) → P.g p = 0 → ∀ {w : ι → ℝ}, P.inner p w = 0 → P.nu p * P.nrm2sq w ≤ P.hessForm p wu, p ∈ 𝓜 with p critical
and h = u - p:
E_h(u) - E_h(p) = ½⟪h, ℋ h⟫_h + β ∑ wᵢ pᵢ hᵢ³ + (β/4) ∑ wᵢ hᵢ⁴.GPDYS.Setting.energy_sub_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p u : ι → ℝ},
P.nrm2sq p = 1 →
P.g p = 0 →
P.nrm2sq u = 1 →
P.energy u - P.energy p =
1 / 2 * P.hessForm p (u - p) + P.β * ∑ i, P.w i * (p i * (u i - p i) ^ 3) +
P.β / 4 * ∑ i, P.w i * (u i - p i) ^ 4ρ = β(3 p h² + h³).def rho (p h : ι → ℝ) : ι → ℝ := fun i => P.β * (3 * p i * h i ^ 2 + h i ^ 3)GPDYS.Setting.rho :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → (ι → ℝ) → (ι → ℝ) → ι → ℝ∇E_h(u) = λ(p) u + ℋ h + ρ for h = u - p, p critical.GPDYS.Setting.gradE_eq_of_critical :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p u : ι → ℝ},
P.g p = 0 → P.gradE u = P.lam p • u + P.hess p (u - p) + P.rho p (u - p)⟪g(u), h⟫_h,
using ⟪u, h⟫_h = ½‖h‖₂²:
⟪g(u), h⟫_h = ⟪h, ℋ h⟫_h + ⟪ρ, h⟫_h - ½‖h‖₂² ⟪ℋ h + ρ, u⟫_h.GPDYS.Setting.inner_g_sub_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p u : ι → ℝ},
P.nrm2sq p = 1 →
P.g p = 0 →
P.nrm2sq u = 1 →
P.inner (P.g u) (u - p) =
P.hessForm p (u - p) + P.inner (P.rho p (u - p)) (u - p) -
1 / 2 * P.nrm2sq (u - p) * P.inner (P.hess p (u - p) + P.rho p (u - p)) uℋ p = 2β p³ for a critical point p.GPDYS.Setting.hess_self :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p : ι → ℝ},
P.g p = 0 → P.hess p p = (2 * P.β) • fun i => p i ^ 3h = (h - c p) + c p.GPDYS.Setting.hessForm_decomp :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p h : ι → ℝ) (c : ℝ),
P.hessForm p h = P.hessForm p (h - c • p) + 2 * c * P.inner (h - c • p) (P.hess p p) + c ^ 2 * P.inner p (P.hess p p)hessForm_sub_ge.GPDYS.Setting.hessForm_sub_ge_aux :
∀ {ν β N3 R HT X Y c : ℝ},
c = -(1 / 2) * R ^ 2 →
ν * (R ^ 2 - c ^ 2) ≤ HT →
0 ≤ Y → |X| ≤ R * (2 * β * N3) → ν * R ^ 2 - ν / 4 * (R ^ 2) ^ 2 - 2 * β * N3 * R ^ 3 ≤ HT + 2 * c * X + c ^ 2 * Y⟪h, ℋ h⟫_h ≥ ν‖h‖₂² - (ν/4)‖h‖₂⁴ - 2β‖p³‖₂ ‖h‖₂³
for h = u - p with u, p ∈ 𝓜.GPDYS.Setting.hessForm_sub_ge :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {p u : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 →
P.nrm2sq u = 1 →
P.nu p * P.nrm2sq (u - p) - P.nu p / 4 * P.nrm2sq (u - p) ^ 2 -
(2 * P.β * P.nrm2 fun i => p i ^ 3) * P.nrm2 (u - p) ^ 3 ≤
P.hessForm p (u - p)vᵢ² ≤ K ‖v‖₂² with K = 1/w_min.GPDYS.Setting.exists_sq_bound :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
∃ K, 0 < K ∧ ∀ (v : ι → ℝ) (i : ι), v i ^ 2 ≤ K * P.nrm2sq v|pᵢ hᵢ| ≤ K ‖h‖₂ for a unit vector p.GPDYS.Setting.abs_mul_le_of_unit :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {K : ℝ},
0 ≤ K →
(∀ (v : ι → ℝ) (i : ι), v i ^ 2 ≤ K * P.nrm2sq v) →
∀ {p : ι → ℝ}, P.nrm2sq p = 1 → ∀ (h : ι → ℝ) (i : ι), |p i * h i| ≤ K * P.nrm2 h|∑ᵢ wᵢ pᵢ hᵢ³| ≤ K ‖h‖₂³ for a unit vector p.GPDYS.Setting.abs_sum_cube_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {K : ℝ},
0 ≤ K →
(∀ (v : ι → ℝ) (i : ι), v i ^ 2 ≤ K * P.nrm2sq v) →
∀ {p : ι → ℝ}, P.nrm2sq p = 1 → ∀ (h : ι → ℝ), |∑ i, P.w i * (p i * h i ^ 3)| ≤ K * P.nrm2 h ^ 3∑ᵢ wᵢ hᵢ⁴ ≤ K ‖h‖₂⁴.GPDYS.Setting.sum_pow_four_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {K : ℝ},
(∀ (v : ι → ℝ) (i : ι), v i ^ 2 ≤ K * P.nrm2sq v) → ∀ (h : ι → ℝ), ∑ i, P.w i * h i ^ 4 ≤ K * P.nrm2sq h ^ 2r > 0 such that
(ν/4)‖u - p‖₂² ≤ E_h(u) - E_h(p) for every u ∈ 𝓜 with ‖u - p‖₂ ≤ r.GPDYS.Setting.local_quadratic_growth :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 →
∃ r,
0 < r ∧
∀ (u : ι → ℝ),
P.nrm2sq u = 1 → P.nrm2 (u - p) ≤ r → P.nu p / 4 * P.nrm2sq (u - p) ≤ P.energy u - P.energy p‖-Δ_h v‖₂ ≤ μ ‖v‖₂ under the Rayleigh bound ⟪·,-Δ_h ·⟫_h ≤ μ ‖·‖₂².GPDYS.Setting.nrm2_negLap_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {μ : ℝ},
0 ≤ μ → (∀ (x : ι → ℝ), P.kin x ≤ μ * P.nrm2sq x) → ∀ (v : ι → ℝ), P.nrm2 (P.negLap v) ≤ μ * P.nrm2 v‖n'(p) v‖₂ ≤ (‖V‖_∞ + 3βK) ‖v‖₂ if pᵢ² ≤ K.GPDYS.Setting.nrm2_nonlin'_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {K : ℝ},
0 ≤ K →
∀ {p : ι → ℝ}, (∀ (i : ι), p i ^ 2 ≤ K) → ∀ (v : ι → ℝ), P.nrm2 (P.nonlin' p v) ≤ (P.Vinf + 3 * P.β * K) * P.nrm2 v‖ℋ v‖₂ ≤ (μ + ‖V‖_∞ + 3βK + λ(p)) ‖v‖₂.GPDYS.Setting.nrm2_hess_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {μ K : ℝ},
0 ≤ μ →
(∀ (x : ι → ℝ), P.kin x ≤ μ * P.nrm2sq x) →
0 ≤ K →
∀ {p : ι → ℝ},
(∀ (i : ι), p i ^ 2 ≤ K) →
∀ (v : ι → ℝ), P.nrm2 (P.hess p v) ≤ (μ + P.Vinf + 3 * P.β * K + P.lam p) * P.nrm2 v‖ρ‖₂ ≤ βK(3‖h‖₂² + ‖h‖₂³) for a unit vector p.GPDYS.Setting.nrm2_rho_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {K : ℝ},
0 ≤ K →
(∀ (v : ι → ℝ) (i : ι), v i ^ 2 ≤ K * P.nrm2sq v) →
∀ {p : ι → ℝ}, P.nrm2sq p = 1 → ∀ (h : ι → ℝ), P.nrm2 (P.rho p h) ≤ P.β * K * (3 * P.nrm2 h ^ 2 + P.nrm2 h ^ 3)⟪ρ, h⟫_h = β (3 ∑ᵢ wᵢ pᵢ hᵢ³ + ∑ᵢ wᵢ hᵢ⁴).GPDYS.Setting.inner_rho_eq :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p h : ι → ℝ),
P.inner (P.rho p h) h = P.β * (3 * ∑ i, P.w i * (p i * h i ^ 3) + ∑ i, P.w i * h i ^ 4)r > 0 such that
E_h(u) - E_h(p) ≤ (1/ν)‖g(u)‖₂² for every u ∈ 𝓜 with ‖u - p‖₂ ≤ r.GPDYS.Setting.local_PL :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 →
∃ r,
0 < r ∧
∀ (u : ι → ℝ),
P.nrm2sq u = 1 → P.nrm2 (u - p) ≤ r → P.energy u - P.energy p ≤ 1 / P.nu p * P.nrm2sq (P.g u)r > 0 of p.GPDYS.Setting.eventually_close :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {μ : ℝ},
0 ≤ μ →
(∀ (v : ι → ℝ), P.kin v ≤ μ * P.nrm2sq v) →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 →
Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds p) →
∀ {r : ℝ}, 0 < r → ∃ K, ∀ (k : ℕ), K ≤ k → P.nrm2 (P.uiter γ u0 k - p) ≤ r0 < η; the upper bound is η_lt_one.GPDYS.Setting.η_pos :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {μ : ℝ},
0 ≤ μ →
(∀ (v : ι → ℝ), P.kin v ≤ μ * P.nrm2sq v) →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 → Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds p) → 0 < GPDYS.η γ μ (P.nu p)GPDYS.Setting.η_lt_one :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {μ : ℝ},
0 ≤ μ →
(∀ (v : ι → ℝ), P.kin v ≤ μ * P.nrm2sq v) →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 → Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds p) → GPDYS.η γ μ (P.nu p) < 1K such that for k ≥ K,
𝓛^{k+1} - E_GS ≤ (1 - η)(𝓛^k - E_GS).GPDYS.Setting.rate_step :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {μ : ℝ},
0 ≤ μ →
(∀ (v : ι → ℝ), P.kin v ≤ μ * P.nrm2sq v) →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 →
Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds p) →
∃ K,
∀ (k : ℕ),
K ≤ k →
P.lyap γ (P.iter γ u0 (k + 1)) - P.energy p ≤
(1 - GPDYS.η γ μ (P.nu p)) * (P.lyap γ (P.iter γ u0 k) - P.energy p)p, and a Rayleigh
bound μ ≥ 0. Then there is an index K such that for every k ≥ K,
𝓛^{k+1} - E_GS ≤ (1-η)(𝓛^k - E_GS) and
E_h(u^k) - E_GS + (R^k)²/γ + (ν/4)‖u^k - u_GS‖₂² ≤ 2(1-η)^{k-K}(𝓛^K - E_GS).GPDYS.Setting.rate_theorem :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {μ : ℝ},
0 ≤ μ →
(∀ (v : ι → ℝ), P.kin v ≤ μ * P.nrm2sq v) →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) →
P.g p = 0 →
Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds p) →
∃ K,
∀ (k : ℕ),
K ≤ k →
P.lyap γ (P.iter γ u0 (k + 1)) - P.energy p ≤
(1 - GPDYS.η γ μ (P.nu p)) * (P.lyap γ (P.iter γ u0 k) - P.energy p) ∧
P.energy (P.uiter γ u0 k) - P.energy p + P.R γ (P.iter γ u0 k) ^ 2 / γ +
P.nu p / 4 * P.nrm2sq (P.uiter γ u0 k - p) ≤
2 * (1 - GPDYS.η γ μ (P.nu p)) ^ (k - K) *
(P.lyap γ (P.iter γ u0 K) - P.energy p)N ≥ 2, and
any Rayleigh bound μ for -Δ_h, the iterates converge to the discrete ground state u_GS,
the constant ν satisfies ν ≥ 2β m_GS² > 0, 0 < η < 1, and the geometric decay (5.6) holds
from some index K on.GPDYS.Setting.rate_theorem' :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∀ {μ : ℝ},
0 ≤ μ →
(∀ (v : ι → ℝ), P.kin v ≤ μ * P.nrm2sq v) →
∃ uGS,
(∀ (i : ι), 0 < uGS i) ∧
P.nrm2 uGS = 1 ∧
P.g uGS = 0 ∧
Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds uGS) ∧
2 * P.β * GPDYS.mGS uGS ^ 2 ≤ P.nu uGS ∧
0 < P.nu uGS ∧
0 < GPDYS.η γ μ (P.nu uGS) ∧
GPDYS.η γ μ (P.nu uGS) < 1 ∧
∃ K,
∀ (k : ℕ),
K ≤ k →
P.lyap γ (P.iter γ u0 (k + 1)) - P.energy uGS ≤
(1 - GPDYS.η γ μ (P.nu uGS)) *
(P.lyap γ (P.iter γ u0 k) - P.energy uGS) ∧
P.energy (P.uiter γ u0 k) - P.energy uGS +
P.R γ (P.iter γ u0 k) ^ 2 / γ +
P.nu uGS / 4 * P.nrm2sq (P.uiter γ u0 k - uGS) ≤
2 * (1 - GPDYS.η γ μ (P.nu uGS)) ^ (k - K) *
(P.lyap γ (P.iter γ u0 K) - P.energy uGS)GPDYS/Spectral.lean — μ_max as the largest eigenvalue of -Δ_h; Theorem 5.1 with μ = μ_max; ν attained2 t c + t² d ≤ 0 for every real t, then c = 0
(the first variation of a quadratic with a maximum at t = 0 vanishes).GPDYS.eq_zero_of_forall_two_mul_add_sq_mul_le :
∀ {c d : ℝ}, (∀ (t : ℝ), 2 * t * c + t ^ 2 * d ≤ 0) → c = 0μ_max = max {⟪v, -Δ_h v⟫_h : v ∈ 𝓜} is the largest eigenvalue
of -Δ_h. The empty-set value is zero.def μmax : ℝ := sSup {x : ℝ | ∃ v : ι → ℝ, P.nrm2sq v = 1 ∧ x = P.kin v}GPDYS.Setting.μmax :
{ι : Type u_1} → [inst : Fintype ι] → [inst_1 : DecidableEq ι] → GPDYS.Setting ι → ℝGPDYS.Setting.kin_continuous :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι), Continuous P.kinGPDYS.Setting.exists_kin_max :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
∃ v, P.nrm2sq v = 1 ∧ ∀ (w : ι → ℝ), P.nrm2sq w = 1 → P.kin w ≤ P.kin vvm ∈ 𝓜 maximizes the Rayleigh quotient on 𝓜, then μ_max = ⟪vm, -Δ_h vm⟫_h.GPDYS.Setting.μmax_eq_kin_of_max :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {vm : ι → ℝ},
P.nrm2sq vm = 1 → (∀ (w : ι → ℝ), P.nrm2sq w = 1 → P.kin w ≤ P.kin vm) → P.μmax = P.kin vmμ_max is attained: μ_max = ⟪v, -Δ_h v⟫_h for some v ∈ 𝓜.GPDYS.Setting.μmax_attained :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
∃ v, P.nrm2sq v = 1 ∧ P.kin v = P.μmax⟪v, -Δ_h v⟫_h ≤ μ_max ‖v‖₂² for every v.GPDYS.Setting.kin_le_μmax :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] (v : ι → ℝ),
P.kin v ≤ P.μmax * P.nrm2sq vGPDYS.Setting.μmax_nonneg :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι], 0 ≤ P.μmaxμ_max is an eigenvalue of -Δ_h: -Δ_h v = μ_max v for a maximizer v ∈ 𝓜 of the
Rayleigh quotient.GPDYS.Setting.μmax_isEigenvalue :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
∃ v, P.nrm2sq v = 1 ∧ P.negLap v = P.μmax • v-Δ_h is at most μ_max.GPDYS.Setting.eigenvalue_le_μmax :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι] {v : ι → ℝ},
v ≠ 0 → ∀ {l : ℝ}, P.negLap v = l • v → l ≤ P.μmaxμ = μ_max, the largest eigenvalue of -Δ_h, exactly as in the paper:
the iterates converge to the discrete ground state u_GS, ν ≥ 2β m_GS² > 0, the rate
η = min{γν/(4(1+γμ_max)), 1/2} satisfies 0 < η < 1, and (5.6) holds from some index K on.GPDYS.Setting.rate_theorem_μmax :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
2 ≤ Fintype.card ι →
∀ {u0 : ι → ℝ},
(∀ (i : ι), 0 < u0 i) →
P.nrm2 u0 = 1 →
∀ {γ : ℝ},
0 < γ →
γ ≤ P.γmax u0 →
∃ uGS,
(∀ (i : ι), 0 < uGS i) ∧
P.nrm2 uGS = 1 ∧
P.g uGS = 0 ∧
Filter.Tendsto (P.uiter γ u0) Filter.atTop (nhds uGS) ∧
2 * P.β * GPDYS.mGS uGS ^ 2 ≤ P.nu uGS ∧
0 < P.nu uGS ∧
0 < GPDYS.η γ P.μmax (P.nu uGS) ∧
GPDYS.η γ P.μmax (P.nu uGS) < 1 ∧
∃ K,
∀ (k : ℕ),
K ≤ k →
P.lyap γ (P.iter γ u0 (k + 1)) - P.energy uGS ≤
(1 - GPDYS.η γ P.μmax (P.nu uGS)) *
(P.lyap γ (P.iter γ u0 k) - P.energy uGS) ∧
P.energy (P.uiter γ u0 k) - P.energy uGS + P.R γ (P.iter γ u0 k) ^ 2 / γ +
P.nu uGS / 4 * P.nrm2sq (P.uiter γ u0 k - uGS) ≤
2 * (1 - GPDYS.η γ P.μmax (P.nu uGS)) ^ (k - K) *
(P.lyap γ (P.iter γ u0 K) - P.energy uGS)w ↦ ⟪w, ℋ w⟫_h is continuous.GPDYS.Setting.hessForm_continuous :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p : ι → ℝ),
Continuous (P.hessForm p)w ↦ ⟪p, w⟫_h is continuous.GPDYS.Setting.inner_continuous :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (p : ι → ℝ),
Continuous fun w => P.inner p wν is attained: it is the minimum of ⟪w, ℋ w⟫_h over the unit tangent vectors w ∈ 𝓜,
⟪p, w⟫_h = 0, as in the paper.GPDYS.Setting.nu_attained :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι),
2 ≤ Fintype.card ι →
∀ {p : ι → ℝ},
P.nrm2sq p = 1 →
(∀ (i : ι), 0 < p i) → P.g p = 0 → ∃ w, P.nrm2sq w = 1 ∧ P.inner p w = 0 ∧ P.hessForm p w = P.nu pGPDYS/Sign.lean — Remark 2.3: uniqueness of the minimizer up to sign (irreducibility from the positive resolvent)i-th component of (M + γ S) x.GPDYS.Setting.MS_mulVec_apply :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (γ : ℝ) (x : ι → ℝ) (i : ι),
(P.M + γ • P.S).mulVec x i = P.w i * x i + γ * ∑ j, P.S i j * x jS (connectivity of the mesh), derived from the entrywise positivity of the
resolvent: for every proper nonempty subset A of the indices there are i ∈ A and j ∉ A with
S i j ≠ 0.GPDYS.Setting.S_irreducible :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) (A : Finset ι),
A.Nonempty → Aᶜ.Nonempty → ∃ i ∈ A, ∃ j ∉ A, P.S i j ≠ 0v has no zero component and vᵀ S v ≤ |v|ᵀ S |v|, then all components of v have the
same sign.GPDYS.Setting.same_sign_of_kin_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {v : ι → ℝ},
(∀ (i : ι), v i ≠ 0) → (P.kin v ≤ P.kin fun i => |v i|) → (∀ (i : ι), 0 < v i) ∨ ∀ (i : ι), v i < 0u > 0 is a critical point of E_h on 𝓜 and
v ∈ 𝓜 satisfies E_h(v) ≤ E_h(u), then v = u or v = -u.GPDYS.Setting.eq_or_eq_neg_of_energy_le :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) {u v : ι → ℝ},
P.nrm2sq u = 1 → (∀ (i : ι), 0 < u i) → P.g u = 0 → P.nrm2sq v = 1 → P.energy v ≤ P.energy u → v = u ∨ v = -uu_GS ∈ 𝓜 which is a critical point of E_h|_𝓜,
the global minimizer of E_h on 𝓜, the unique nonnegative critical point, and the minimizer is
unique up to sign: every minimizer of E_h on 𝓜 is u_GS or -u_GS.GPDYS.Setting.exists_groundState_sign :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (P : GPDYS.Setting ι) [Nonempty ι],
∃ uGS,
(∀ (i : ι), 0 < uGS i) ∧
P.nrm2 uGS = 1 ∧
P.g uGS = 0 ∧
(∀ (v : ι → ℝ), P.nrm2 v = 1 → P.energy uGS ≤ P.energy v) ∧
(∀ (v : ι → ℝ), P.nrm2 v = 1 → (∀ (i : ι), 0 ≤ v i) → P.g v = 0 → v = uGS) ∧
∀ (v : ι → ℝ), P.nrm2 v = 1 → P.energy v ≤ P.energy uGS → v = uGS ∨ v = -uGS