The given inverse deformation defines the exact equivalences used by the Piola packet construction.

The actual high/corrector pair, with all potential regularity derived from the high field.

noncomputable def EulerPacketConstructedPiola.normal (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (m₀ y : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Normal, given by (F y).symm.toContinuousLinearMap.adjoint m₀.

Equations

• EulerPacketConstructedPiola.normal F m₀ y = (ContinuousLinearMap.adjoint ↑(F y).symm) m₀

theorem EulerPacketConstructedPiola.normal_ne_zero (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (m₀ : EulerSmoothLimit.Space) (hm₀ : m₀ ≠ 0) (y : EulerSmoothLimit.Space) : normal F m₀ y ≠ 0

noncomputable def EulerPacketConstructedPiola.corrector (P : ℝ) [Fact (0 < P)] (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (m₀ : EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space

Corrector, given by liftedSlowCurl P F (field P (normal F m₀) A).

Equations

• EulerPacketConstructedPiola.corrector P F m₀ A = EulerPacketPiola.liftedSlowCurl P F (EulerPacketPeriodicPotential.field P (EulerPacketConstructedPiola.normal F m₀) A)

noncomputable def EulerPacketConstructedPiola.pairLp (P : ℝ) [Fact (0 < P)] (κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hAc : HasCompactSupport A) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hN : ContDiff ℝ (↑⊤) (normal F m₀)) (hm₀ : m₀ ≠ 0) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P A x)) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (θ : ℝ) in 0..P, A (y, ↑θ) = 0) (p : ℕ) : ↥(EulerLiftedGradientSpace.LiftL2 P)

Pair Lᵖ, constructed using piolaPairLp.

Equations

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

theorem EulerPacketConstructedPiola.pairLp_mem (P : ℝ) [Fact (0 < P)] (κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hAc : HasCompactSupport A) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hN : ContDiff ℝ (↑⊤) (normal F m₀)) (hm₀ : m₀ ≠ 0) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P A x)) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (θ : ℝ) in 0..P, A (y, ↑θ) = 0) (p : ℕ) : pairLp P κ m₀ Ξ A hΞ hAc F hN hm₀ hA hmean p ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ m₀

theorem EulerPacketConstructedPiola.pairLp_ae (P : ℝ) [Fact (0 < P)] (κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hAc : HasCompactSupport A) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hN : ContDiff ℝ (↑⊤) (normal F m₀)) (hm₀ : m₀ ≠ 0) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P A x)) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (θ : ℝ) in 0..P, A (y, ↑θ) = 0) (hF : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ Ξ y = ↑(F y)) (hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ↑(F y)) = 1) (htan : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), inner ℝ (normal F m₀ x.1) (A x) = 0) (p : ℕ) : ↑↑(pairLp P κ m₀ Ξ A hΞ hAc F hN hm₀ hA hmean p) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => (F x.1).symm (κ ^ p • A x + κ ^ (p + 1) • corrector P F m₀ A x)

The entire pair is the literal source formula, as an actual divergence-free L² field.

noncomputable def EulerTransversePacketProvider.Data.deformationEquiv {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space

Deformation equiv, given by ContinuousLinearEquiv.equivOfInverse (D.F.field t x) (D.FInv.field t x) (D.inverse_left t x) (D.inverse_right t x).

Equations

• D.deformationEquiv t x = ContinuousLinearEquiv.equivOfInverse ((D.F.field t) x) ((D.FInv.field t) x) ⋯ ⋯

@[simp]

theorem EulerTransversePacketProvider.Data.deformationEquiv_coe {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ↑(D.deformationEquiv t x) = (D.F.field t) x

@[simp]

theorem EulerTransversePacketProvider.Data.deformationEquiv_symm_coe {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ↑(D.deformationEquiv t x).symm = (D.FInv.field t) x

@[simp]

theorem EulerTransversePacketProvider.Data.deformationEquiv_normal {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) : EulerPacketConstructedPiola.normal (D.deformationEquiv t) D.m₀ = ⇑(D.normal.field t)

theorem EulerTransversePacketProvider.Data.initialNormal_ne_zero {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : D.m₀ ≠ 0