MatrixFlow.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SharpLiebThirring.ODEProof.bounded_ode_exists line 21

Source documentation

Bounded globally Lipschitz fields have solutions on the entire prescribed compact interval. There is no restriction on the length of the interval.

lemma bounded_ode_exists {E : Type u148} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {l r : ℝ} (hlr : l ≤ r) (x₀ : E) (f : ℝ → E → E) (K L : ℝ≥0)
    (hK : ∀ t ∈ Icc l r, LipschitzWith K (f t))
    (hc : ∀ x, ContinuousOn (fun t ↦ f t x) (Icc l r))
    (hL : ∀ t ∈ Icc l r, ∀ x, ‖f t x‖ ≤ L) :
    ∃ x : ℝ → E, x l = x₀ ∧ ∀ t ∈ Icc l r, HasDerivWithinAt x (f t (x t)) (Icc l r) t := by
…

lemma OAI.SharpLiebThirring.ODEProof.derivative_right_of_Icc line 38

lemma OAI.SharpLiebThirring.ODEProof.bounded_ode_perturbation line 44

Source documentation

Uniform perturbation estimate for solutions, including both endpoint times.

lemma bounded_ode_perturbation {E : Type u150} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {l r : ℝ} {f g : ℝ → E → E} {x y : ℝ → E} {K : ℝ≥0} {η : ℝ}
    (hK : ∀ t, LipschitzWith K (g t))
    (hx : ∀ t ∈ Icc l r, HasDerivWithinAt x (f t (x t)) (Icc l r) t)
    (hy : ∀ t ∈ Icc l r, HasDerivWithinAt y (g t (y t)) (Icc l r) t)
    (hxy : x l = y l)
    (herr : ∀ t ∈ Icc l r, ∀ z, dist (f t z) (g t z) ≤ η) :
    ∀ t ∈ Icc l r, dist (x t) (y t) ≤ gronwallBound 0 K η (t-l) := by
…

lemma OAI.SharpLiebThirring.ODEProof.bounded_ode_unique line 62

lemma OAI.SharpLiebThirring.ODEProof.continuous_solution_family line 78

Source documentation

Continuous parameter dependence, uniform even when the evaluation time varies.

lemma continuous_solution_family {E : Type u152} {P : Type u153} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [TopologicalSpace P] {l r : ℝ} {f : P → ℝ → E → E} {x : P → ℝ → E}
    (K : P → ℝ≥0) (η : P → P → ℝ)
    (hK : ∀ p t, LipschitzWith (K p) (f p t))
    (hx : ∀ p t, t ∈ Icc l r → HasDerivWithinAt (x p) (f p t (x p t)) (Icc l r) t)
    (hinit : ∀ p q, x p l = x q l)
    (hη : ∀ p, Continuous (fun q ↦ η q p)) (hη0 : ∀ p, η p p = 0)
    (hηpos : ∀ p q, 0 ≤ η p q)
    (herr : ∀ p q t, t ∈ Icc l r → ∀ z, dist (f p t z) (f q t z) ≤ η p q) :
    Continuous (fun z : P × Icc l r ↦ x z.1 z.2) := by
…

lemma OAI.SharpLiebThirring.ODEProof.affine_forcing_exists_family line 116

Source documentation

Ready-to-use parameterized affine forcing in a bounded Lipschitz field.

lemma affine_forcing_exists_family {E : Type u154} {P : Type u155} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] [TopologicalSpace P] {l r : ℝ} (hlr : l ≤ r) (x₀ : E)
    (M : E → E) (K B : ℝ≥0) (hK : LipschitzWith K M) (hB : ∀ x, ‖M x‖ ≤ B)
    (a : P → ℝ) (ha : Continuous a) (v : P → C(Icc l r,E)) (hv : Continuous v) :
    ∃ x : P → ℝ → E, (∀ p, x p l = x₀) ∧
      (∀ p t (ht : t ∈ Icc l r), HasDerivWithinAt (x p)
        (a p • M (x p t) + v p ⟨t,ht⟩) (Icc l r) t) ∧
      Continuous (fun z : P × Icc l r ↦ x z.1 z.2) := by
…

abbrev OAI.SharpLiebThirring.MatrixFlow.Sym line 171
def OAI.SharpLiebThirring.MatrixFlow.symInclude line 172
instance OAI.SharpLiebThirring.MatrixFlow.(instance at line 176) line 176
def OAI.SharpLiebThirring.MatrixFlow.symDiag line 179
def OAI.SharpLiebThirring.MatrixFlow.symOuter line 180
lemma OAI.SharpLiebThirring.MatrixFlow.symOuter_apply line 182
def OAI.SharpLiebThirring.MatrixFlow.symEntry line 185
lemma OAI.SharpLiebThirring.MatrixFlow.symEntry_apply line 190
lemma OAI.SharpLiebThirring.MatrixFlow.continuous_symOuter line 191
def OAI.SharpLiebThirring.MatrixFlow.symConj line 196
lemma OAI.SharpLiebThirring.MatrixFlow.symConj_apply line 205
lemma OAI.SharpLiebThirring.MatrixFlow.symConj_val line 207
lemma OAI.SharpLiebThirring.MatrixFlow.sign_sq line 210
lemma OAI.SharpLiebThirring.MatrixFlow.sign_diagonal_unitary line 212
lemma OAI.SharpLiebThirring.MatrixFlow.norm_symConj line 220
lemma OAI.SharpLiebThirring.MatrixFlow.symConj_diag line 225
lemma OAI.SharpLiebThirring.MatrixFlow.symConj_outer line 236
lemma OAI.SharpLiebThirring.MatrixFlow.zero_row_sign line 240
lemma OAI.SharpLiebThirring.MatrixFlow.fixed_reflection_offdiag line 243
lemma OAI.SharpLiebThirring.MatrixFlow.matrix_norm_entry line 250
def OAI.SharpLiebThirring.MatrixFlow.matrixForcing line 265
Source documentation
The outer-product forcing, viewed in the supremum-norm space on the time interval.
```
def matrixForcing (ε : ℝ) {l r : ℝ} (u : ℝ → Fin N → ℝ)
    (hu : ContinuousOn u (Icc l r)) (C : Matrix (Fin N) (Fin N) ℝ) : C(Icc l r, Sym N) :=
…
```
Mentions: OAI.SharpLiebThirring.MatrixFlow.Sym
lemma OAI.SharpLiebThirring.MatrixFlow.continuous_matrixForcing line 270
def OAI.SharpLiebThirring.MatrixFlow.flowRhs line 278
lemma OAI.SharpLiebThirring.MatrixFlow.flowRhs_lipschitz line 282
lemma OAI.SharpLiebThirring.MatrixFlow.matrix_flow_exists line 293
lemma OAI.SharpLiebThirring.MatrixFlow.matrix_rowSign_mulVec line 307
lemma OAI.SharpLiebThirring.MatrixFlow.flowRhs_equivariant line 315
lemma OAI.SharpLiebThirring.MatrixFlow.matrix_flow_equivariant line 322
def OAI.SharpLiebThirring.MatrixFlow.symCongr line 342
lemma OAI.SharpLiebThirring.MatrixFlow.symCongr_apply line 356
lemma OAI.SharpLiebThirring.MatrixFlow.symCongr_outer line 359
lemma OAI.SharpLiebThirring.MatrixFlow.integral_outer_identity line 364
lemma OAI.SharpLiebThirring.MatrixFlow.integral_outer_mulVec line 376
lemma OAI.SharpLiebThirring.MatrixFlow.integrate_affine_ode line 387
lemma OAI.SharpLiebThirring.MatrixFlow.flow_integral_sub line 405
lemma OAI.SharpLiebThirring.MatrixFlow.flow_integral_identity line 416
lemma OAI.SharpLiebThirring.MatrixFlow.gram_entry_bound line 441
lemma OAI.SharpLiebThirring.MatrixFlow.bounded_integral_norm line 453
lemma OAI.SharpLiebThirring.MatrixFlow.matching_gram_norm line 462