The constructed Hilbert operator for the transverse displacement form

The time primitive will be substituted for J in TransverseVariationalInverse. This file constructs, rather than assumes, the inverse of the actual operator I - J* H J. Its coercivity follows from the potential upper bound and the primitive estimate. No inverse, solution, or weak equation is an input.

noncomputable def EulerTransverseVariationalInverse.dirichletOperator {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) : V →L[ℝ] V

The operator representing the kinetic form minus the actual potential form.

Equations

• EulerTransverseVariationalInverse.dirichletOperator J H = ContinuousLinearMap.id ℝ V - ContinuousLinearMap.adjoint J ∘SL H ∘SL J

theorem EulerTransverseVariationalInverse.dirichletOperator_inner {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) (u v : V) : inner ℝ ((dirichletOperator J H) u) v = inner ℝ u v - inner ℝ (H (J u)) (J v)

This is precisely the displacement variational form.

theorem EulerTransverseVariationalInverse.dirichletOperator_coercive {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) (L K : ℝ) (hK : 0 ≤ K) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ L * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hsmall : K * L ≤ 1 / 2) (u : V) : 1 / 2 * ‖u‖ ^ 2 ≤ inner ℝ ((dirichletOperator J H) u) u

The primitive estimate and the one-sided potential bound prove coercivity.

noncomputable def EulerTransverseVariationalInverse.dirichletSolver {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) (L K : ℝ) (hK : 0 ≤ K) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ L * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hsmall : K * L ≤ 1 / 2) : W →L[ℝ] V

The actual forcing-to-derivative solution map constructed by Lax--Milgram.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerTransverseVariationalInverse.dirichletSolver_weak {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) (L K : ℝ) (hK : 0 ≤ K) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ L * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hsmall : K * L ≤ 1 / 2) (f : W) (v : V) : have u := (dirichletSolver J H L K hK hJ hH hsmall) f; inner ℝ u v - inner ℝ (H (J u)) (J v) = -inner ℝ f (J v)

The constructed solution obeys the actual weak displacement equation.

theorem EulerTransverseVariationalInverse.dirichletSolver_unique {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) (L K : ℝ) (hK : 0 ≤ K) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ L * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hsmall : K * L ≤ 1 / 2) (f : W) (u : V) (hu : ∀ (v : V), inner ℝ u v - inner ℝ (H (J u)) (J v) = -inner ℝ f (J v)) : u = (dirichletSolver J H L K hK hJ hH hsmall) f

No other derivative in the same Hilbert displacement space solves this form.

theorem EulerTransverseVariationalInverse.dirichletSolver_norm {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) (L K : ℝ) (hK : 0 ≤ K) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ L * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hsmall : K * L ≤ 1 / 2) (f : W) : ‖(dirichletSolver J H L K hK hJ hH hsmall) f‖ ≤ 2 * ‖J‖ * ‖f‖

Quantitative boundedness of the genuinely constructed solution map.

theorem EulerTransverseVariationalInverse.existsUnique_dirichlet_solution {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] (J : V →L[ℝ] W) (H : W →L[ℝ] W) (L K : ℝ) (hK : 0 ≤ K) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ L * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hsmall : K * L ≤ 1 / 2) (f : W) : ∃! u : V, ∀ (v : V), inner ℝ u v - inner ℝ (H (J u)) (J v) = -inner ℝ f (J v)

Existence and uniqueness, as conclusions from coefficient and primitive bounds.

theorem EulerTransverseVariationalInverse.timeMultiplier_quadratic_upper {W : Type u_2} [NormedAddCommGroup W] [InnerProductSpace ℝ W] (T : ℝ) (hT : 0 ≤ T) (H : C(↑(Set.Icc 0 T), W →L[ℝ] W)) (K : ℝ) (hH : ∀ (t : ↑(Set.Icc 0 T)) (w : W), inner ℝ ((H t) w) w ≤ K * ‖w‖ ^ 2) (u : ↥(EulerTimeLp.TimeLp T W)) : inner ℝ ((EulerTimeLp.timeMultiplier T hT H) u) u ≤ K * ‖u‖ ^ 2

A pointwise upper bound on the given time-dependent Hessian gives the actual Bochner-space quadratic-form upper bound.