The mean displacement form with its initial boundary operator

The operator is constructed as I - J* H J + R* C R, where J is the actual displacement primitive and R its initial trace. The boundary lower bound is required only on the trace image, as in the source's solenoidal space.

noncomputable def EulerMeanVariationalOperator.meanOperator {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) : V →L[ℝ] V

The actual bounded operator representing kinetic, potential, and boundary terms.

Equations

• EulerMeanVariationalOperator.meanOperator J R H C = EulerTransverseVariationalInverse.dirichletOperator J H + ContinuousLinearMap.adjoint R ∘SL C ∘SL R

theorem EulerMeanVariationalOperator.meanOperator_inner {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) (u v : V) : inner ℝ ((meanOperator J R H C) u) v = inner ℝ u v - inner ℝ (H (J u)) (J v) + inner ℝ (C (R u)) (R v)

The constructed operator has exactly the intended bilinear form.

theorem EulerMeanVariationalOperator.meanOperator_coercive {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) (P Q K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ P * ‖u‖ ^ 2) (hR : ∀ (u : V), ‖R u‖ ^ 2 ≤ Q * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hC : ∀ (u : V), -B * ‖R u‖ ^ 2 ≤ inner ℝ (C (R u)) (R u)) (hsmall : K * P + B * Q ≤ 1 / 2) (u : V) : 1 / 2 * ‖u‖ ^ 2 ≤ inner ℝ ((meanOperator J R H C) u) u

The source's two time estimates and coefficient bounds prove coercivity.

noncomputable def EulerMeanVariationalOperator.meanSolver {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) (P Q K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ P * ‖u‖ ^ 2) (hR : ∀ (u : V), ‖R u‖ ^ 2 ≤ Q * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hC : ∀ (u : V), -B * ‖R u‖ ^ 2 ≤ inner ℝ (C (R u)) (R u)) (hsmall : K * P + B * Q ≤ 1 / 2) : W →L[ℝ] V

The forcing-to-derivative map constructed from the coercive mean form.

Equations

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

theorem EulerMeanVariationalOperator.meanSolver_weak {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) (P Q K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ P * ‖u‖ ^ 2) (hR : ∀ (u : V), ‖R u‖ ^ 2 ≤ Q * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hC : ∀ (u : V), -B * ‖R u‖ ^ 2 ≤ inner ℝ (C (R u)) (R u)) (hsmall : K * P + B * Q ≤ 1 / 2) (f : W) (v : V) : have u := (meanSolver J R H C P Q K B hK hB hJ hR hH hC hsmall) f; inner ℝ u v - inner ℝ (H (J u)) (J v) + inner ℝ (C (R u)) (R v) = -inner ℝ f (J v)

The actual weak equation follows from the constructed inverse.

theorem EulerMeanVariationalOperator.meanSolver_unique {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) (P Q K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ P * ‖u‖ ^ 2) (hR : ∀ (u : V), ‖R u‖ ^ 2 ≤ Q * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hC : ∀ (u : V), -B * ‖R u‖ ^ 2 ≤ inner ℝ (C (R u)) (R u)) (hsmall : K * P + B * Q ≤ 1 / 2) (f : W) (u : V) (hu : ∀ (v : V), inner ℝ u v - inner ℝ (H (J u)) (J v) + inner ℝ (C (R u)) (R v) = -inner ℝ f (J v)) : u = (meanSolver J R H C P Q K B hK hB hJ hR hH hC hsmall) f

Uniqueness holds in the same actual Hilbert displacement space.

theorem EulerMeanVariationalOperator.meanSolver_norm {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) (P Q K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ P * ‖u‖ ^ 2) (hR : ∀ (u : V), ‖R u‖ ^ 2 ≤ Q * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hC : ∀ (u : V), -B * ‖R u‖ ^ 2 ≤ inner ℝ (C (R u)) (R u)) (hsmall : K * P + B * Q ≤ 1 / 2) (f : W) : ‖(meanSolver J R H C P Q K B hK hB hJ hR hH hC hsmall) f‖ ≤ 2 * ‖J‖ * ‖f‖

The derivative bound is polynomial in the primitive norm.

theorem EulerMeanVariationalOperator.existsUnique_mean_solution {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (J : V →L[ℝ] W) (R : V →L[ℝ] X) (H : W →L[ℝ] W) (C : X →L[ℝ] X) (P Q K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hJ : ∀ (u : V), ‖J u‖ ^ 2 ≤ P * ‖u‖ ^ 2) (hR : ∀ (u : V), ‖R u‖ ^ 2 ≤ Q * ‖u‖ ^ 2) (hH : ∀ (w : W), inner ℝ (H w) w ≤ K * ‖w‖ ^ 2) (hC : ∀ (u : V), -B * ‖R u‖ ^ 2 ≤ inner ℝ (C (R u)) (R u)) (hsmall : K * P + B * Q ≤ 1 / 2) (f : W) : ∃! u : V, ∀ (v : V), inner ℝ u v - inner ℝ (H (J u)) (J v) + inner ℝ (C (R u)) (R v) = -inner ℝ f (J v)

Existence and uniqueness are conclusions, with no solution or inverse hypothesis.