Gradient Flow

Results named in Tau Ceti's TauCeti.Analysis.GradientFlow modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremDe Giorgi energy identity#

Let φ be lower semicontinuous at x with φ(x) ≠ ⊤, and let y r ∈ J_r x be a resolvent step for every time r ∈ (0, σ], with φ_σ(x) ≠ ⊥. Then φ_σ(x) + ∫₀^σ d(x, y r)² / (2r²) dr = φ(x).

TauCeti.moreauYosida_add_integral_eq.{u_1} {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal}
  {x : X} {y : ℝ → X} {σ : ℝ} (hφ : LowerSemicontinuousAt φ x) (hσ : 0 < σ)
  (hy : ∀ r ∈ Set.Ioc 0 σ, y r ∈ TauCeti.moreauYosidaResolvent φ r.toNNReal x) (hx : φ x ≠ ⊤)
  (hσ' : TauCeti.moreauYosida φ σ.toNNReal x ≠ ⊥) :
  TauCeti.moreauYosida φ σ.toNNReal x +
      ↑(∫ (r : ℝ) in 0..σ, (edist x (y r)).toReal ^ 2 / (2 * r ^ 2)) =
    φ x
Lean

Formalized in Tau Ceti as TauCeti.moreauYosida_add_integral_eq.

Sources
LeanTauCeti.moreauYosida_add_integral_eq

TheoremDe Giorgi energy inequality#

Let y r ∈ J_r x be a resolvent step for every time r ∈ (0, σ], with φ(x) ≠ ⊤ and φ_σ(x) ≠ ⊥. Then φ_σ(x) + ∫₀^σ d(x, y r)² / (2r²) dr ≤ φ(x). Equality holds when φ is lower semicontinuous at x (TauCeti.moreauYosida_add_integral_eq).

TauCeti.moreauYosida_add_integral_le.{u_1} {X : Type u_1} [PseudoEMetricSpace X] {φ : X → EReal}
  {x : X} {y : ℝ → X} {σ : ℝ} (hσ : 0 < σ)
  (hy : ∀ r ∈ Set.Ioc 0 σ, y r ∈ TauCeti.moreauYosidaResolvent φ r.toNNReal x) (hx : φ x ≠ ⊤)
  (hσ' : TauCeti.moreauYosida φ σ.toNNReal x ≠ ⊥) :
  TauCeti.moreauYosida φ σ.toNNReal x +
      ↑(∫ (r : ℝ) in 0..σ, (edist x (y r)).toReal ^ 2 / (2 * r ^ 2)) ≤
    φ x
Lean

Formalized in Tau Ceti as TauCeti.moreauYosida_add_integral_le.

Sources
LeanTauCeti.moreauYosida_add_integral_le

TheoremHölder estimate for the piecewise constant interpolant#

Under the hypotheses of TauCeti.edist_sq_le_of_forall_mem_moreauYosidaResolvent, the piecewise constant interpolant t ↦ u ⌈t / τ⌉₊ of a minimizing movement sequence satisfies, for 0 ≤ s ≤ t, d(u ⌈s / τ⌉₊, u ⌈t / τ⌉₊)² ≤ 2 (t - s + τ) (E - A) (1 + exp (8 (t + τ) / τ')). As τ → 0 this becomes a 1/2-Hölder bound on bounded time intervals.

TauCeti.edist_ceil_sq_le_of_forall_mem_moreauYosidaResolvent.{u_1} {X : Type u_1}
  [PseudoEMetricSpace X] {φ : X → EReal} {τ τ' : NNReal} {u : ℕ → X}
  (hu : ∀ (n : ℕ), u (n + 1) ∈ TauCeti.moreauYosidaResolvent φ τ (u n)) (hτ : 0 < τ)
  (hττ' : 4 * τ ≤ τ') {A E : ℝ} (hA : TauCeti.moreauYosida φ τ' (u 0) = ↑A) (hE : φ (u 0) = ↑E)
  {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) :
  edist (u ⌈s / ↑τ⌉₊) (u ⌈t / ↑τ⌉₊) ^ 2 ≤
    ENNReal.ofReal (2 * (t - s + ↑τ) * (E - A) * (1 + Real.exp (8 * (t + ↑τ) / ↑τ')))
Lean

Formalized in Tau Ceti as TauCeti.edist_ceil_sq_le_of_forall_mem_moreauYosidaResolvent.

Sources
LeanTauCeti.edist_ceil_sq_le_of_forall_mem_moreauYosidaResolvent
Uses 1
Proof usesDiscrete Grönwall bound under coercivity

TheoremYoung's inequality along a curve#

the integral of g (u r) |u'|(r) is at most the dissipation.

AbsolutelyContinuousOnInterval.lintegral_mul_metricDerivative_le_dissipation.{u_1} {X : Type u_1}
  [PseudoMetricSpace X] {p q : ℝ} {g : X → ENNReal} {u : ℝ → X} {s t : ℝ}
  (hpq : p.HolderConjugate q) (hu : AbsolutelyContinuousOnInterval u s t) :
  ∫⁻ (r : ℝ) in Set.uIoc s t, g (u r) * TauCeti.metricDerivative u r ≤
    TauCeti.dissipation p q g u s t
Lean

Formalized in Tau Ceti as AbsolutelyContinuousOnInterval.lintegral_mul_metricDerivative_le_dissipation.

Sources
LeanAbsolutelyContinuousOnInterval.lintegral_mul_metricDerivative_le_dissipation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.