LeanPool.NavierStokesAndEuler.Euler.PacketSourceCorrectionCoefficients

The correction coefficients constructed from the prescribed deformation. The order-zero terms have the positive sign of the transformed equation; the correction source subsequently applies the negative pressure projection.

source

noncomputable def EulerPacketCorrectionCoefficients.rawFrame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) :

EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space

Raw frame, given by D.F.field (D.clamp z.1) z.2.1.

Equations

EulerPacketCorrectionCoefficients.rawFrame D z = (D.F.field (D.clamp z.1)) z.2.1

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.rawFrameTime {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) :

EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space

Raw frame time, given by D.F₁.field (D.clamp z.1) z.2.1.

Equations

EulerPacketCorrectionCoefficients.rawFrameTime D z = (D.F₁.field (D.clamp z.1)) z.2.1

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.rawInverse {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) :

EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space

Raw inverse, given by D.FInv.field (D.clamp z.1) z.2.1.

Equations

EulerPacketCorrectionCoefficients.rawInverse D z = (D.FInv.field (D.clamp z.1)) z.2.1

Instances For

source

def EulerPacketCorrectionCoefficients.frameCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) :

EulerPacketCylinderField.MatrixCoefficient D.T (rawFrame D)

Frame coefficient, bundling path, orbit, raw_eq.

Equations

EulerPacketCorrectionCoefficients.frameCoefficient D = { path := D.F.field, orbit := ⋯, raw_eq := ⋯ }

Instances For

source

def EulerPacketCorrectionCoefficients.frameTimeCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) :

EulerPacketCylinderField.MatrixCoefficient D.T (rawFrameTime D)

Frame time coefficient, bundling path, orbit, raw_eq.

Equations

EulerPacketCorrectionCoefficients.frameTimeCoefficient D = { path := D.F₁.field, orbit := ⋯, raw_eq := ⋯ }

Instances For

source

def EulerPacketCorrectionCoefficients.inverseCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) :

EulerPacketCylinderField.MatrixCoefficient D.T (rawInverse D)

Inverse coefficient, bundling path, orbit, raw_eq.

Equations

EulerPacketCorrectionCoefficients.inverseCoefficient D = { path := D.FInv.field, orbit := ⋯, raw_eq := ⋯ }

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.rawMetric {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) :

EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space

Raw metric, given by (rawInverse D z).comp (rawInverse D z).adjoint.

Equations

EulerPacketCorrectionCoefficients.rawMetric D z = EulerPacketCorrectionCoefficients.rawInverse D z ∘SL ContinuousLinearMap.adjoint (EulerPacketCorrectionCoefficients.rawInverse D z)

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.rawInverseMetric {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) :

EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space

Raw inverse metric, given by (rawFrame D z).adjoint.comp (rawFrame D z).

Equations

EulerPacketCorrectionCoefficients.rawInverseMetric D z = ContinuousLinearMap.adjoint (EulerPacketCorrectionCoefficients.rawFrame D z) ∘SL EulerPacketCorrectionCoefficients.rawFrame D z

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.rawLinear {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (z : EulerPacketPointJets.Domain) :

EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space

Raw linear, given by (2 : ℝ) • (rawInverse D z).comp (rawFrameTime D z).

Equations

EulerPacketCorrectionCoefficients.rawLinear D z = 2 • EulerPacketCorrectionCoefficients.rawInverse D z ∘SL EulerPacketCorrectionCoefficients.rawFrameTime D z

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.rawQuadratic {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (i : Fin 3) (z : EulerPacketPointJets.Domain) :

EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space

Raw quadratic, given by κ • (rawInverse D z).comp (fderiv ℝ (fun x => rawFrame D (z.1,(x,z.2.2))) z.2.1 (EuclideanSpace.single i 1)).

Equations

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

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.metricCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) :

EulerPacketCylinderField.MatrixCoefficient D.T (rawMetric D)

Metric coefficient, given by (inverseCoefficient D).comp (inverseCoefficient D).adjoint.

Equations

EulerPacketCorrectionCoefficients.metricCoefficient D = (EulerPacketCorrectionCoefficients.inverseCoefficient D).comp (EulerPacketCorrectionCoefficients.inverseCoefficient D).adjoint

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.inverseMetricCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) :

EulerPacketCylinderField.MatrixCoefficient D.T (rawInverseMetric D)

Inverse metric coefficient, given by (frameCoefficient D).adjoint.comp (frameCoefficient D).

Equations

EulerPacketCorrectionCoefficients.inverseMetricCoefficient D = (EulerPacketCorrectionCoefficients.frameCoefficient D).adjoint.comp (EulerPacketCorrectionCoefficients.frameCoefficient D)

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.linearCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) :

EulerPacketCylinderField.MatrixCoefficient D.T (rawLinear D)

Linear coefficient, given by ((inverseCoefficient D).comp (frameTimeCoefficient D)).smul 2.

Equations

EulerPacketCorrectionCoefficients.linearCoefficient D = ((EulerPacketCorrectionCoefficients.inverseCoefficient D).comp (EulerPacketCorrectionCoefficients.frameTimeCoefficient D)).smul 2

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.quadraticCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (i : Fin 3) :

EulerPacketCylinderField.MatrixCoefficient D.T (rawQuadratic D κ i)

Quadratic coefficient, given by ((inverseCoefficient D).comp ((frameCoefficient D).spatialDerivative (EuclideanSpace.single i 1))).smul κ.

Equations

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

Instances For

source

@[simp]

theorem EulerPacketCorrectionCoefficients.metricCoefficient_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

((metricCoefficient D).path t) x = (D.FInv.field t) x ∘SL ContinuousLinearMap.adjoint ((D.FInv.field t) x)

source

@[simp]

theorem EulerPacketCorrectionCoefficients.inverseMetricCoefficient_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

((inverseMetricCoefficient D).path t) x = ContinuousLinearMap.adjoint ((D.F.field t) x) ∘SL (D.F.field t) x

source

@[simp]

theorem EulerPacketCorrectionCoefficients.linearCoefficient_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

((linearCoefficient D).path t) x = 2 • (D.FInv.field t) x ∘SL (D.F₁.field t) x

source

theorem EulerPacketCorrectionCoefficients.quadraticCoefficient_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (κ : ℝ) (i : Fin 3) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

((quadraticCoefficient D κ i).path t) x = κ • (D.FInv.field t) x ∘SL (fderiv ℝ (⇑(D.F.field t)) x) (EuclideanSpace.single i 1)

source

noncomputable def EulerPacketCorrectionCoefficients.metricTower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] :

EulerAllOrderCorrectionData.CoefficientTower P D.T

Metric tower, given by (metricCoefficient D).toCoefficientTower P.

Equations

EulerPacketCorrectionCoefficients.metricTower D P = EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower P (EulerPacketCorrectionCoefficients.metricCoefficient D)

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.inverseMetricTower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] :

EulerAllOrderCorrectionData.CoefficientTower P D.T

Inverse metric tower, given by (inverseMetricCoefficient D).toCoefficientTower P.

Equations

EulerPacketCorrectionCoefficients.inverseMetricTower D P = EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower P (EulerPacketCorrectionCoefficients.inverseMetricCoefficient D)

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.linearTower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] :

EulerAllOrderCorrectionData.CoefficientTower P D.T

Linear tower, given by (linearCoefficient D).toCoefficientTower P.

Equations

EulerPacketCorrectionCoefficients.linearTower D P = EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower P (EulerPacketCorrectionCoefficients.linearCoefficient D)

Instances For

source

noncomputable def EulerPacketCorrectionCoefficients.quadraticTower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (i : Fin 3) :

EulerAllOrderCorrectionData.CoefficientTower P D.T

Quadratic tower, given by (quadraticCoefficient D κ i).toCoefficientTower P.

Equations

EulerPacketCorrectionCoefficients.quadraticTower D P κ i = EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower P (EulerPacketCorrectionCoefficients.quadraticCoefficient D κ i)

Instances For

source

@[simp]

theorem EulerPacketCorrectionCoefficients.metricTower_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) :

((metricTower D P).coefficient t).coefficient x = (D.FInv.field t) x.1 ∘SL ContinuousLinearMap.adjoint ((D.FInv.field t) x.1)

source

@[simp]

theorem EulerPacketCorrectionCoefficients.inverseMetricTower_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) :

((inverseMetricTower D P).coefficient t).coefficient x = ContinuousLinearMap.adjoint ((D.F.field t) x.1) ∘SL (D.F.field t) x.1

source

@[simp]

theorem EulerPacketCorrectionCoefficients.linearTower_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) :

((linearTower D P).coefficient t).coefficient x = 2 • (D.FInv.field t) x.1 ∘SL (D.F₁.field t) x.1

source

theorem EulerPacketCorrectionCoefficients.quadraticTower_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (i : Fin 3) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) :

((quadraticTower D P κ i).coefficient t).coefficient x = κ • (D.FInv.field t) x.1 ∘SL (fderiv ℝ (⇑(D.F.field t)) x.1) (EuclideanSpace.single i 1)

source

theorem EulerPacketCorrectionCoefficients.metricTower_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] :

Continuous fun (t : ↑(Set.Icc 0 D.T)) => ((metricTower D P).coefficient t).operator

source

theorem EulerPacketCorrectionCoefficients.inverseMetricTower_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] :

Continuous fun (t : ↑(Set.Icc 0 D.T)) => ((inverseMetricTower D P).coefficient t).operator