Explicit polynomial bounds for the actual mean Gram and time-form inverse constants, derived from a determinant-one parent deformation.

@[instance_reducible]

noncomputable def EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity3 : NormedAddCommGroup (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity4 : NormedSpace ℝ (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ (solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerPacketParentMeanCoercivity.instPacketParentMeanCoercivity4 = inferInstance

def EulerPacketParentMeanCoercivity.gramInverseEnvelope (C : ℝ) : ℝ

Gram inverse envelope, given by (3*C^2+1)^2.

Equations

• EulerPacketParentMeanCoercivity.gramInverseEnvelope C = (3 * C ^ 2 + 1) ^ 2

def EulerPacketParentMeanCoercivity.transportEnvelope (C C₁ : ℝ) : ℝ

Transport envelope, given by 1+(2*(gramInverseEnvelope C)^2*C^2*C₁+gramInverseEnvelope C*C₁)+gramInverseEnvelope C*C.

Equations

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

def EulerPacketParentMeanCoercivity.inverseEnvelope (C C₁ : ℝ) : ℝ

Inverse envelope, given by 2*(transportEnvelope C C₁)^2.

Equations

• EulerPacketParentMeanCoercivity.inverseEnvelope C C₁ = 2 * EulerPacketParentMeanCoercivity.transportEnvelope C C₁ ^ 2

theorem EulerPacketParentMeanCoercivity.transportEnvelope_nonneg (C C₁ : ℝ) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) : 0 ≤ transportEnvelope C C₁

theorem EulerPacketParentMeanCoercivity.inverseEnvelope_nonneg (C C₁ : ℝ) : 0 ≤ inverseEnvelope C C₁

theorem EulerPacketParentMeanCoercivity.inverseOperator_norm (D : EulerMeanPacketProvider.Data) (C : ℝ) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) : ‖D.opInv‖ ≤ 3 * C ^ 2

theorem EulerPacketParentMeanCoercivity.gramInverse_bound (D : EulerMeanPacketProvider.Data) (C : ℝ) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) : D.frameLower⁻¹ ≤ gramInverseEnvelope C

theorem EulerPacketParentMeanCoercivity.transport_bound (D : EulerMeanPacketProvider.Data) (C C₁ : ℝ) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) (hF₁ : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F₁.field t) x‖ ≤ C₁) (hT : D.T ≤ 1) : EulerMeanVariationalInverse.meanTransportCost D.T D.opInv D.opF D.opF₁ ≤ transportEnvelope C C₁

theorem EulerPacketParentMeanCoercivity.sourceInverse_bound (D : EulerMeanPacketProvider.Data) (C C₁ : ℝ) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) (hF₁ : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F₁.field t) x‖ ≤ C₁) (hT : D.T ≤ 1) : (EulerMeanSourceFixedInverse.sourceFixedCoercivity D.T D.F D.F₁ D.opInv)⁻¹ ≤ inverseEnvelope C C₁