Weighted bounds for the literal signed cross-covariance defect #
The covariance class follows from the actual supported harmonic families. The requested moving stress preserves the residual class. Their difference is retained on every band; only the supplied tail identity makes it vanish.
theorem
NavierStokes.SignedCrossDefectClass.primary_bounds
{D ι : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α δ β η : ℝ}
(f : LabelSumBounds.SignedFamily s P α δ β η)
(hαδ : α ≤ δ)
(i : Fin 3)
(j : ℤ)
:
LabelSumBounds.UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => ((f.primary l).velocity n i).coeff j x
The primary coefficient bound is recovered from the old coefficient
and the actual old-minus-primary bound in SignedFamily.
theorem
NavierStokes.SignedCrossDefectClass.crossTensor_mem
{D ι : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α δ β η : ℝ}
(f : LabelSumBounds.SignedFamily s P α δ β η)
(a : SignedMeanGain.Assembly f)
(hαδ : α ≤ δ)
:
SignedMeanGain.TensorClass s (α + β) (SignedMeanGain.crossTensor f a)
The actual covariance of the two assembled fields has the sum of their exponents. Native support eliminates cross-label products.
theorem
NavierStokes.SignedCrossDefectClass.physicalSigma_mem
(G : SignedMeanGain.Geometry)
(e : ℕ)
{r : MeanIncrementBounds.Field Point}
{α : ℝ}
(hr : MeanIncrementBounds.SmoothOn G.domain r)
(hs : ∀ (n : ℕ), LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (r n))
(hc : WeightedClasses.MeanClass G.strip α r)
:
The actual moving primitive retains the exact radial weight and costs no band exponent.
theorem
NavierStokes.SignedCrossDefectClass.defect_mem
(G : SignedMeanGain.Geometry)
{ι : Type}
{P : ι → ℕ → Point → ℝ}
{α δ β η : ℝ}
(f : LabelSumBounds.SignedFamily G.strip P α δ β η)
(a : SignedMeanGain.Assembly f)
(hαδ : α ≤ δ)
(i j : Fin 3)
(e : ℕ)
(r : MeanIncrementBounds.Field Point)
(hS : MeanIncrementBounds.SmoothOn G.domain (SignedMeanGain.crossTensor f a i j))
(hr : MeanIncrementBounds.SmoothOn G.domain r)
(hs : ∀ (n : ℕ), LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (r n))
(hc : WeightedClasses.MeanClass G.strip (α + β) r)
:
WeightedClasses.MeanClass G.strip (α + β)
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a i j) - SignedMeanGain.physicalSigma G e r)
A baseline class for the literal cross defect. There is no covariance cancellation hypothesis, either on the initial bands or on the tail.
theorem
NavierStokes.SignedCrossDefectClass.defect_all_exponents
(G : SignedMeanGain.Geometry)
{ι : Type}
{P : ι → ℕ → Point → ℝ}
{α δ β η : ℝ}
(f : LabelSumBounds.SignedFamily G.strip P α δ β η)
(a : SignedMeanGain.Assembly f)
(hαδ : α ≤ δ)
(i j : Fin 3)
(e : ℕ)
(r : MeanIncrementBounds.Field Point)
(hS : MeanIncrementBounds.SmoothOn G.domain (SignedMeanGain.crossTensor f a i j))
(hr : MeanIncrementBounds.SmoothOn G.domain r)
(hs : ∀ (n : ℕ), LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (r n))
(hc : WeightedClasses.MeanClass G.strip (α + β) r)
(N : ℕ)
(htail :
∀ (n : ℕ),
N ≤ n →
∀ x ∈ G.strip.domain,
StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a i j) n x = SignedMeanGain.physicalSigma G e r n x)
(γ : ℝ)
:
The same fixed finite-head cutoff yields every exponent. The only equality premise is the actual covariance identity on the tail.
theorem
NavierStokes.SignedCrossDefectClass.actual_defect_mem
(G : SignedMeanGain.Geometry)
{ι : Type}
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(i j : Fin 3)
(e : ℕ)
(r : MeanIncrementBounds.Field Point)
(hS : MeanIncrementBounds.SmoothOn G.domain (SignedMeanGain.crossTensor f a i j))
(hr : SignedMeanGain.MovingField G r)
(hc : WeightedClasses.MeanClass G.strip (1 + σ - κ) r)
:
WeightedClasses.MeanClass G.strip (1 + σ - κ)
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a i j) - SignedMeanGain.physicalSigma G e r)
Specialization to the exponents of the actual signed step.
theorem
NavierStokes.SignedCrossDefectClass.residual_defects_mem
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{ι : Type}
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j))
(hθreg : SignedMeanGain.MovingField G (u.thetaResidual c))
(hzreg : SignedMeanGain.MovingField G (u.axialResidual c))
(hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c))
:
WeightedClasses.MeanClass G.strip (1 + σ - κ)
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 1) - SignedMeanGain.physicalSigma G 2 (u.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (1 + σ - κ)
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 2) - SignedMeanGain.physicalSigma G 1 (u.axialResidual c))
Both literal defects of the signed mean update have the baseline residual exponent, with no discarded initial bands.
theorem
NavierStokes.SignedCrossDefectClass.residual_defects_all_exponents
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{ι : Type}
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j))
(hθreg : SignedMeanGain.MovingField G (u.thetaResidual c))
(hzreg : SignedMeanGain.MovingField G (u.axialResidual c))
(hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c))
(N : ℕ)
(htail :
∀ (n : ℕ),
N ≤ n →
∀ x ∈ G.strip.domain,
∀ (i : Fin 2),
StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 i.succ) n x = LocalSignedRequest.requestedStress G.patch G.coord c u n x i)
(γ : ℝ)
:
WeightedClasses.MeanClass G.strip γ
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 1) - SignedMeanGain.physicalSigma G 2 (u.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip γ
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 2) - SignedMeanGain.physicalSigma G 1 (u.axialResidual c))
The requested-stress identity is required only for bands n ≥ N.
The literal defects remain present on all earlier bands, in every class.
theorem
NavierStokes.SignedCrossDefectClass.residual_defects_all_exponents_of_primitive
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{ι : Type}
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j))
(H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u)
(hfixed : (VariableGaugeMean.reconstructState G.gauge c u).pressure = u.pressure)
(hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c))
(N : ℕ)
(htail :
∀ (n : ℕ),
N ≤ n →
∀ x ∈ G.strip.domain,
∀ (i : Fin 2),
StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 i.succ) n x = LocalSignedRequest.requestedStress G.patch G.coord c u n x i)
(γ : ℝ)
:
WeightedClasses.MeanClass G.strip γ
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 1) - SignedMeanGain.physicalSigma G 2 (u.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip γ
(StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 2) - SignedMeanGain.physicalSigma G 1 (u.axialResidual c))
Primitive incoming fields and the actual reconstructed pressure give the residual regularity needed by the preceding theorem.