Inverse Regularity

noncomputable def EulerInverseRegularity.differenceQuotient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (τ : E →L[ℝ] E) (h : ℝ) : E →L[ℝ] E

The bounded translation difference quotient with increment h.

Equations

• EulerInverseRegularity.differenceQuotient τ h = h⁻¹ • (τ - ContinuousLinearMap.id ℝ E)

def EulerInverseRegularity.commutator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D T : E →L[ℝ] E) : E →L[ℝ] E

The operator commutator D T minus T D.

Equations

• EulerInverseRegularity.commutator D T = D ∘SL T - T ∘SL D

def EulerInverseRegularity.iteratedRingCommutator {R : Type u_2} [Ring R] (D T : R) : ℕ → R

Repeated commutation with an operator, defined by its actual algebraic formula.

Equations

• EulerInverseRegularity.iteratedRingCommutator D T 0 = T
• EulerInverseRegularity.iteratedRingCommutator D T n.succ = D * EulerInverseRegularity.iteratedRingCommutator D T n - EulerInverseRegularity.iteratedRingCommutator D T n * D

theorem EulerInverseRegularity.mul_iteratedRingCommutator {R : Type u_2} [Ring R] (D T : R) (n : ℕ) : D * iteratedRingCommutator D T n = iteratedRingCommutator D T n * D + iteratedRingCommutator D T (n + 1)

theorem EulerInverseRegularity.iterated_operator_leibniz {R : Type u_2} [Ring R] (D T : R) (n : ℕ) : D ^ n * T = ∑ l ∈ Finset.range (n + 1), n.choose l • (iteratedRingCommutator D T l * D ^ (n - l))

The complete noncommutative Leibniz formula, proved from the commutator definition.

theorem EulerInverseRegularity.inverse_commutator_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T D : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (f : E) : D ((EulerCoerciveProjection.coerciveInverse T c hc hT) f) = (EulerCoerciveProjection.coerciveInverse T c hc hT) (D f - (commutator D T) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f))

theorem EulerInverseRegularity.inverse_commutator_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T D : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (f : E) : ‖D ((EulerCoerciveProjection.coerciveInverse T c hc hT) f)‖ ≤ c⁻¹ * (‖D f‖ + ‖(commutator D T) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f)‖)

theorem EulerInverseRegularity.inverse_iterated_commutator_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T D : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (f : E) (n : ℕ) : (D ^ (n + 1)) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f) = (EulerCoerciveProjection.coerciveInverse T c hc hT) ((D ^ (n + 1)) f - ∑ l ∈ Finset.range (n + 1), (n + 1).choose (l + 1) • (iteratedRingCommutator D T (l + 1)) ((D ^ (n - l)) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f)))

The full differentiated inverse recurrence, derived from the operator equation.

theorem EulerInverseRegularity.inverse_iterated_commutator_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T D : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (f : E) (n : ℕ) : ‖(D ^ (n + 1)) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f)‖ ≤ c⁻¹ * (‖(D ^ (n + 1)) f‖ + ∑ l ∈ Finset.range (n + 1), ↑((n + 1).choose (l + 1)) * ‖iteratedRingCommutator D T (l + 1)‖ * ‖(D ^ (n - l)) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f)‖)

The quantitative all-order recurrence follows from the exact commutator identity.

theorem EulerInverseRegularity.differenceQuotient_commutator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (τ T : E →L[ℝ] E) (h : ℝ) : commutator (differenceQuotient τ h) T = h⁻¹ • commutator τ T

theorem EulerInverseRegularity.inverse_differenceQuotient_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T τ : E →L[ℝ] E) (h c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (f : E) : ‖(differenceQuotient τ h) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f)‖ ≤ c⁻¹ * (‖(differenceQuotient τ h) f‖ + ‖h⁻¹ • (commutator τ T) ((EulerCoerciveProjection.coerciveInverse T c hc hT) f)‖)

The spatial difference-quotient estimate, before any passage to weak derivatives.

theorem EulerInverseRegularity.coerciveInverse_eq_mapInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) : EulerCoerciveProjection.coerciveInverse T c hc hT = T.inverse

theorem EulerInverseRegularity.coerciveInverse_eq_ringInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) : EulerCoerciveProjection.coerciveInverse T c hc hT = Ring.inverse T

theorem EulerInverseRegularity.contDiff_coerciveInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ → E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (t : ℝ) (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ ((T t) x) x) {n : WithTop ℕ∞} (hreg : ContDiff ℝ n T) : ContDiff ℝ n fun (t : ℝ) => EulerCoerciveProjection.coerciveInverse (T t) c hc ⋯

A Cⁿ family of coercive operators has a Cⁿ family of the constructed inverses.

theorem EulerInverseRegularity.hasDerivAt_coerciveInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ → E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (t : ℝ) (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ ((T t) x) x) (t : ℝ) (T₁ : E →L[ℝ] E) (hder : HasDerivAt T T₁ t) : HasDerivAt (fun (s : ℝ) => EulerCoerciveProjection.coerciveInverse (T s) c hc ⋯) (-EulerCoerciveProjection.coerciveInverse (T t) c hc ⋯ ∘SL T₁ ∘SL EulerCoerciveProjection.coerciveInverse (T t) c hc ⋯) t

The time derivative of the constructed inverse is -I T' I.

theorem EulerInverseRegularity.hasDerivAt_coerciveSolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ → E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (t : ℝ) (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ ((T t) x) x) (f : ℝ → E) (t : ℝ) (T₁ : E →L[ℝ] E) (f₁ : E) (hder : HasDerivAt T T₁ t) (hf : HasDerivAt f f₁ t) : HasDerivAt (fun (s : ℝ) => (EulerCoerciveProjection.coerciveInverse (T s) c hc ⋯) (f s)) ((EulerCoerciveProjection.coerciveInverse (T t) c hc ⋯) (f₁ - T₁ ((EulerCoerciveProjection.coerciveInverse (T t) c hc ⋯) (f t)))) t

theorem EulerInverseRegularity.contDiff_projectedOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : ℝ → E →L[ℝ] E) {n : WithTop ℕ∞} (hreg : ContDiff ℝ n G) : ContDiff ℝ n fun (t : ℝ) => EulerCoerciveProjection.projectedOperator S (G t)

theorem EulerInverseRegularity.hasDerivAt_projectedOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : ℝ → E →L[ℝ] E) (t : ℝ) (G₁ : E →L[ℝ] E) (hder : HasDerivAt G G₁ t) : HasDerivAt (fun (s : ℝ) => EulerCoerciveProjection.projectedOperator S (G s)) (EulerCoerciveProjection.projectedOperator S G₁) t

theorem EulerInverseRegularity.contDiff_projectedInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : ℝ → E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (t : ℝ) (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ ((G t) x) x) {n : WithTop ℕ∞} (hreg : ContDiff ℝ n G) : ContDiff ℝ n fun (t : ℝ) => EulerCoerciveProjection.projectedInverse S (G t) c hc ⋯

theorem EulerInverseRegularity.hasDerivAt_projectedInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : ℝ → E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (t : ℝ) (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ ((G t) x) x) (t : ℝ) (G₁ : E →L[ℝ] E) (hder : HasDerivAt G G₁ t) : HasDerivAt (fun (s : ℝ) => EulerCoerciveProjection.projectedInverse S (G s) c hc ⋯) (-EulerCoerciveProjection.projectedInverse S (G t) c hc ⋯ ∘SL EulerCoerciveProjection.projectedOperator S G₁ ∘SL EulerCoerciveProjection.projectedInverse S (G t) c hc ⋯) t