Genuine mean and high constraints for the joined recursively constructed family.
theorem
EulerPacketCylinderField.joinedSource_corrector_eq
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{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τ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hc : primary.corrector = D.curlCorrector P primary.high)
(p : ℕ)
(hp : 1 ≤ p)
:
(joinedSourceProfiles P M D τ hτ hτT B primary p).corrector = D.curlCorrector P (joinedSourceProfiles P M D τ hτ hτT B primary p).high
theorem
EulerPacketCylinderField.joinedSource_high_mean_zero
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hm : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, primary.high (↑t, x, θ) = 0)
(p : ℕ)
(hp : 1 ≤ p)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketCylinderField.joinedSource_high_tangent_all
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(ht :
∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (D.normalField (↑t, x, θ)) (primary.high (↑t, x, θ)) = 0)
(p : ℕ)
(hp : 1 ≤ p)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
noncomputable def
EulerPacketCylinderField.joinedMeanPullbackField
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(p : ℕ)
:
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
((joinedSourceOperators P M D τ hτ hτT B).inverseFrame z) ((joinedSourceProfiles P M D τ hτ hτT B primary p).mean z)
Joined mean pullback field as an element of Field P M.T (fun z => (joinedSourceOperators P M D τ hτ hτT B).inverseFrame z ((joinedSourceProfiles P M D τ hτ hτT B primary p).mean z)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.joinedMeanPullback_divergence
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hmean : primary.mean = 0)
(A : SourceCoefficientAgreement M D)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
:
EulerSmoothLimit.divergence
(fun (y : EulerSmoothLimit.Space) =>
((joinedSourceOperators P M D τ hτ hτT B).inverseFrame (↑t, y, 0))
((joinedSourceProfiles P M D τ hτ hτT B primary p).mean (↑t, y, 0)))
x = 0
theorem
EulerPacketCylinderField.joinedMeanPullbackField_mem
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hmean : primary.mean = 0)
(A : SourceCoefficientAgreement M D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
:
(joinedMeanPullbackField P M D hT τ hτ hτT B primary hprimary p).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ m