LeanPool.NavierStokesAndEuler.Euler.PacketPhysicalCorrectionPotential

The signed pressure correction has a genuine scalar potential in physical coordinates. Its gradient is exactly the inverse-transpose reconstruction used in the quantitative correction estimates.

source

noncomputable def EulerAllOrderDriftCorrection.Budget.physicalPotential {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {A : EulerAllOrderCorrectionData.Data P D.T} (B : Budget P ⋯ A) (k : ℝ) (Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 D.T)) :

EulerSmoothLimit.Space → ℝ

Physical potential, given by B.normalizedGraphPotential P k t ∘ Y t.

Equations

EulerAllOrderDriftCorrection.Budget.physicalPotential D P B k Y t = EulerAllOrderDriftCorrection.Budget.normalizedGraphPotential P B k t ∘ Y t

Instances For

source

theorem EulerAllOrderDriftCorrection.Budget.physicalPotential_joint_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {A : EulerAllOrderCorrectionData.Data P D.T} (B : Budget P ⋯ A) (k : ℝ) (Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : Continuous (Function.uncurry Y)) :

Continuous (Function.uncurry (physicalPotential D P B k Y))

source

theorem EulerAllOrderDriftCorrection.Budget.physicalPotential_smooth {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {A : EulerAllOrderCorrectionData.Data P D.T} (B : Budget P ⋯ A) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 D.T)) :

ContDiff ℝ (↑⊤) (physicalPotential D P B k Y t)

source

theorem EulerAllOrderDriftCorrection.Budget.physicalPotential_gradient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {A : EulerAllOrderCorrectionData.Data P D.T} (B : Budget P ⋯ A) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

gradient (physicalPotential D P B k Y t) x = A.κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y t x))) (pointPressure P B t (EulerGraphPressurePotential.cylinderGraph P k A.direction (Y t x)))

source

theorem EulerAllOrderDriftCorrection.Budget.physicalPotential_gradient_jet {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {A : EulerAllOrderCorrectionData.Data P D.T} (B : Budget P ⋯ A) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (k : ℝ) (hk : k * A.κ = 1) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

iteratedFDeriv ℝ n (gradient (physicalPotential D P B k Y t)) x = iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => A.κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y t y))) (pointPressure P B t (EulerGraphPressurePotential.cylinderGraph P k A.direction (Y t y)))) x

source

theorem EulerAllOrderDriftCorrection.Budget.physicalPotential_hessian_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {A : EulerAllOrderCorrectionData.Data P D.T} (B : Budget P ⋯ A) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

‖fderiv ℝ (gradient (physicalPotential D P B k Y t)) x‖ = ‖iteratedFDeriv ℝ 1 (fun (y : EulerSmoothLimit.Space) => A.κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y t y))) (pointPressure P B t (EulerGraphPressurePotential.cylinderGraph P k A.direction (Y t y)))) x‖