Documentation

LeanPool.NavierStokesAndEuler.Euler.TransverseCoordinateRegularity

Genuine time-H¹ transverse coordinates #

The coordinates are obtained by applying the constructed frame left inverse to the physical displacement. Their time derivative is an actual Bochner L² field, and differentiating the reconstructed displacement gives the exact kinetic coordinate identity used in the strong transverse equation.

source
noncomputable def EulerTransverseCoordinateRegularity.coordinatePrimitive {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (u : ↥(EulerTimeLp.TimeLp T E)) :
ℝ → U

Canonical coordinates obtained from the actual inverse Gram coefficient.

Equations
Instances For
    source
    noncomputable def EulerTransverseCoordinateRegularity.coordinateDerivative {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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (u : ↥(EulerTimeLp.TimeLp T E)) :
    ↥(EulerTimeLp.TimeLp T U)

    The actual L² derivative of the canonical coordinates.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem EulerTransverseCoordinateRegularity.coordinatePrimitive_absolutelyContinuous {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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) :
      AbsolutelyContinuousOnInterval (coordinatePrimitive T hT Q c hc hQ u) 0 T

      The canonical coordinates are genuinely absolutely continuous.

      source
      theorem EulerTransverseCoordinateRegularity.coordinatePrimitive_hasDerivAt_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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) :
      ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (coordinatePrimitive T hT Q c hc hQ u) (↑↑(coordinateDerivative T hT Q Q₁ c hc hQ u) t) t

      The explicitly constructed L² field is the actual a.e. coordinate derivative.

      source
      theorem EulerTransverseCoordinateRegularity.terminalPrimitive_coordinateDerivative {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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) :
      ((EulerTerminalTimePrimitive.terminalPrimitive T hT) (coordinateDerivative T hT Q Q₁ c hc hQ u)) t = coordinatePrimitive T hT Q c hc hQ u ↑t

      Integrating the coordinate derivative recovers the canonical coordinates.

      source
      theorem EulerTransverseCoordinateRegularity.coordinatePrimitive_initial {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (m : ↑(Set.Icc 0 T) → E) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) :
      coordinatePrimitive T hT Q c hc hQ (↑u) 0 = 0

      The initial coordinate trace vanishes for every admissible displacement.

      source
      theorem EulerTransverseCoordinateRegularity.coordinatePrimitive_terminal {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (u : ↥(EulerTimeLp.TimeLp T E)) :
      coordinatePrimitive T hT Q c hc hQ u T = 0

      The terminal coordinate trace vanishes identically.

      source
      theorem EulerTransverseCoordinateRegularity.coordinatePrimitive_reconstruct_of_range {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (u : ↥(EulerTimeLp.TimeLp T E)) (huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T u ↑t) (t : ↑(Set.Icc 0 T)) :
      (Q t) (coordinatePrimitive T hT Q c hc hQ u ↑t) = EulerTerminalTimePrimitive.realPrimitive T u ↑t

      Reconstruction only requires the prescribed physical displacement to lie in the actual range of the frame. This general statement also applies to infinite-dimensional spatial constraint spaces.

      source
      theorem EulerTransverseCoordinateRegularity.coordinateDerivative_reconstruct_of_range {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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) (huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T u ↑t) :
      (EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) (coordinateDerivative T hT Q Q₁ c hc hQ u) = u

      The kinetic identity follows from injectivity of the genuine time primitive.

      source
      theorem EulerTransverseCoordinateRegularity.coordinatePrimitive_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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) :
      ↑↑((EulerTerminalTimePrimitive.primitiveTimeLp T hT) (coordinateDerivative T hT Q Q₁ c hc hQ u)) =ᵐ[EulerTimeLp.timeMeasure T] coordinatePrimitive T hT Q c hc hQ u

      The L² primitive of the coordinate derivative has the actual coordinate path as its representative.

      source
      theorem EulerTransverseCoordinateRegularity.coordinateDerivative_reconstruct_ae_of_range {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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) (huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T u ↑t) :
      ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, ↑↑u t = (EulerVolterraConvolution.extendPath T hT Q₁ t) (coordinatePrimitive T hT Q c hc hQ u t) + (EulerVolterraConvolution.extendPath T hT Q t) (↑↑(coordinateDerivative T hT Q Q₁ c hc hQ u) t)

      The physical derivative has the literal expression Q_t ξ + Q ξ_t a.e.

      source
      theorem EulerTransverseCoordinateRegularity.transverse_range {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (m : ↑(Set.Icc 0 T) → E) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) (t : ↑(Set.Icc 0 T)) :
      ∃ (x : U), (Q t) x = EulerTerminalTimePrimitive.realPrimitive T ↑u ↑t

      A transverse constraint puts the physical displacement in the frame's range.

      source
      theorem EulerTransverseCoordinateRegularity.coordinatePrimitive_reconstruct {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (m : ↑(Set.Icc 0 T) → E) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) (t : ↑(Set.Icc 0 T)) :
      (Q t) (coordinatePrimitive T hT Q c hc hQ ↑u ↑t) = EulerTerminalTimePrimitive.realPrimitive T ↑u ↑t

      Canonical coordinates reconstruct every admissible transverse displacement.

      source
      theorem EulerTransverseCoordinateRegularity.coordinateDerivative_reconstruct {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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (m : ↑(Set.Icc 0 T) → E) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) :
      (EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) (coordinateDerivative T hT Q Q₁ c hc hQ ↑u) = ↑u

      The transverse derivative is the derivative of its reconstructed coordinates.

      source
      theorem EulerTransverseCoordinateRegularity.coordinateDerivative_reconstruct_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 Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (m : ↑(Set.Icc 0 T) → E) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) :
      ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, ↑↑↑u t = (EulerVolterraConvolution.extendPath T hT Q₁ t) (coordinatePrimitive T hT Q c hc hQ (↑u) t) + (EulerVolterraConvolution.extendPath T hT Q t) (↑↑(coordinateDerivative T hT Q Q₁ c hc hQ ↑u) t)

      The transverse physical derivative has its actual coordinate expression a.e.