Total raw-field provider for a positive history time

Every admissible input is sent to the constructed history/forward solution. Its raw PDE, tangent constraint, parity, actual Field witnesses, true time derivative, pressure gradient and literal curl corrector are all exported.

theorem EulerTransversePacketProvider.Forcing.path_unique {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G H : Forcing P D raw) : G.path = H.path

The genuine cylinder forcing path is determined by its prescribed raw field.

theorem EulerTransversePacketJoin.vector_independent_of_witness {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G H : EulerTransversePacketProvider.Forcing P D raw) : vector τ hτ hτT B G = vector τ hτ hτT B H

theorem EulerTransversePacketJoin.scalar_independent_of_witness {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G H : EulerTransversePacketProvider.Forcing P D raw) : scalar τ hτ hτT B G = scalar τ hτ hτT B H

theorem EulerTransversePacketJoin.vector_tangent {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : inner ℝ (D.normalField (↑t, x, θ)) (vector τ hτ hτT B G (↑t, x, θ)) = 0

noncomputable def EulerTransversePacketJoin.highSolve {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (raw : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField × EulerPacketProfileRecursion.ScalarField

The total high operator, backed by the unique genuine solution on admissible inputs.

Equations

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

theorem EulerTransversePacketJoin.highSolve_of_admissible {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : highSolve τ hτ hτT B raw = (vector τ hτ hτT B (Classical.choice h), scalar τ hτ hτT B (Classical.choice h))

theorem EulerTransversePacketJoin.highSolve_eq {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : highSolve τ hτ hτT B raw = (vector τ hτ hτT B G, scalar τ hτ hτT B G)

noncomputable def EulerTransversePacketJoin.highVectorField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : EulerPacketCylinderField.Field P D.T (highSolve τ hτ hτT B raw).1

High vector field, given by (vectorField τ hτ hτT B (Classical.choice h)).congr (fun t x θ => by rw [highSolve_of_admissible τ hτ hτT B h]).

Equations

• EulerTransversePacketJoin.highVectorField τ hτ hτT B h = (EulerTransversePacketJoin.vectorField τ hτ hτT B (Classical.choice h)).congr ⋯

noncomputable def EulerTransversePacketJoin.highDerivativeField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : EulerPacketCylinderField.Field P D.T (vectorDerivative τ hτ hτT B (Classical.choice h))

High derivative field, given by vectorDerivativeField τ hτ hτT B (Classical.choice h).

Equations

• EulerTransversePacketJoin.highDerivativeField τ hτ hτT B h = EulerTransversePacketJoin.vectorDerivativeField τ hτ hτT B (Classical.choice h)

theorem EulerTransversePacketJoin.highVectorField_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : EulerPacketCylinderField.TimeDerivative ⋯ (highVectorField τ hτ hτT B h) (highDerivativeField τ hτ hτT B h)

noncomputable def EulerTransversePacketJoin.highPressureGradientField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : EulerPacketCylinderField.Field P D.T (EulerPacketCylinderField.pressureGradient (highSolve τ hτ hτT B raw).2)

High pressure gradient field, given by (scalarGradientField τ hτ hτT B (Classical.choice h)).congr (fun t x θ => by rw [highSolve_of_admissible τ hτ hτT B h]).

Equations

• EulerTransversePacketJoin.highPressureGradientField τ hτ hτT B h = (EulerTransversePacketJoin.scalarGradientField τ hτ hτT B (Classical.choice h)).congr ⋯

noncomputable def EulerTransversePacketJoin.highCorrectorField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : EulerPacketCylinderField.Field P D.T (D.curlCorrector P (highSolve τ hτ hτT B raw).1)

High corrector field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketJoin.highCorrectorField τ hτ hτT B h = { path := EulerTransversePacketJoin.correctorPath τ hτ hτT B (Classical.choice h), orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerTransversePacketJoin.highCorrectorDerivativeField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : EulerPacketCylinderField.Field P D.T (correctorDerivative τ hτ hτT B (Classical.choice h))

High corrector derivative field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketJoin.highCorrectorDerivativeField τ hτ hτT B h = { path := EulerTransversePacketJoin.correctorTimePath τ hτ hτT B (Classical.choice h), orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketJoin.highCorrectorField_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) : EulerPacketCylinderField.TimeDerivative ⋯ (highCorrectorField τ hτ hτT B h) (highCorrectorDerivativeField τ hτ hτT B h)

theorem EulerTransversePacketJoin.highSolve_equation {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (highSolve τ hτ hτT B raw).1 (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet (highSolve τ hτ hτT B raw).2 (↑t, x, θ)) = raw (↑t, x, θ)

theorem EulerTransversePacketJoin.highSolve_parity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (h : Nonempty (EulerTransversePacketProvider.Forcing P D raw)) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) : (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (highSolve τ hτ hτT B raw).1 (↑t, -x, -θ) = -(highSolve τ hτ hτT B raw).1 (↑t, x, θ)) ∧ ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (highSolve τ hτ hτT B raw).2 (↑t, -x, -θ) = (highSolve τ hτ hτT B raw).2 (↑t, x, θ)