The actual Gram inverse on Bochner L²

The multiplier Gram operator inherits the pointwise lower frame bound. Its coercive inverse equals multiplication by the previously constructed matrix/Hilbert Gram inverse. This identifies the strong-equation inverse with the same operator to which the genuine parameter estimates apply.

noncomputable def EulerTimeLpGramInverse.gramOperator {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ↥(EulerTimeLp.TimeLp T U) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)

The genuine Bochner Gram operator, formed from the actual frame multiplier.

Equations

• EulerTimeLpGramInverse.gramOperator T hT Q = ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT Q) ∘SL EulerTimeLp.timeMultiplier T hT Q

theorem EulerTimeLpGramInverse.gramOperator_coercive {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (u : ↥(EulerTimeLp.TimeLp T U)) : c * ‖u‖ ^ 2 ≤ inner ℝ ((gramOperator T hT Q) u) u

The pointwise lower frame bound gives coercivity on the actual time-L² space.

noncomputable def EulerTimeLpGramInverse.gramSolver {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : ↥(EulerTimeLp.TimeLp T U) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)

The actual coercive inverse of the time Gram operator.

Equations

• EulerTimeLpGramInverse.gramSolver T hT Q c hc hQ = EulerCoerciveProjection.coerciveInverse (EulerTimeLpGramInverse.gramOperator T hT Q) c hc ⋯

theorem EulerTimeLpGramInverse.gramOperator_ae {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (u : ↥(EulerTimeLp.TimeLp T U)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, ↑↑((gramOperator T hT Q) u) t = (ContinuousLinearMap.adjoint (Q (Set.projIcc 0 T hT t))) ((Q (Set.projIcc 0 T hT t)) (↑↑u t))

The Gram operator is pointwise Q*Q, with genuine Bochner representatives.

theorem EulerTimeLpGramInverse.gramSolver_eq_multiplier {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : gramSolver T hT Q c hc hQ = EulerTimeLp.timeMultiplier T hT (EulerTransverseGramPath.gramInversePath T Q c hc hQ)

The actual coercive inverse equals the pointwise inverse used in the strong equation.

theorem EulerTimeLpGramInverse.gramSolver_norm {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : ‖gramSolver T hT Q c hc hQ‖ ≤ c⁻¹

The lower frame bound controls the true operator inverse.

theorem EulerTimeLpGramInverse.gramOperator_contDiff {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (Q : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) : ContDiff ℝ n fun (x : P) => gramOperator T hT (Q x)

Actual smoothness of the time Gram operator follows from the coefficient path.

theorem EulerTimeLpGramInverse.gramOperator_bound {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (Q : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hQ : ContDiff ℝ (↑⊤) Q) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => gramOperator T hT (Q y)) x‖ ≤ 3 * C ^ 2 * EulerGevrey.majorant R 0 n

The actual Gram coefficient jets have a polynomial factorial multiplier constant.