Exact transport of mean bounds and residual coefficient classes #
Pullback along e : D ≃ₗᵢ[ℝ] E uses the actual state/context construction
from StateReindex. Every derivative norm and every scalar majorant is
unchanged. In particular, uniform constants are chosen before the label
both before and after reassociation.
theorem
NavierStokes.MeanBoundsReindex.strip_roundtrip
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
(s : WeightedClasses.StripData D)
:
theorem
NavierStokes.MeanBoundsReindex.majorant_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
(s : WeightedClasses.StripData E)
(w : ℕ → E → ℝ)
(α C : ℝ)
(p n : ℕ)
(x : D)
:
WeightedClasses.majorant (ParticularWaveBounds.reindexStrip e s) (fun (k : ℕ) (y : D) => w k (e y)) α C p n x = WeightedClasses.majorant s w α C p n (e x)
theorem
NavierStokes.MeanBoundsReindex.finiteJet_bound_pull_iff
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(e : D ≃ₗᵢ[ℝ] E)
(s : WeightedClasses.StripData E)
(w : ℕ → E → ℝ)
(f : ℕ → E → F)
(α C : ℝ)
(p m : ℕ)
:
(∀ (n : ℕ),
∀ x ∈ (ParticularWaveBounds.reindexStrip e s).domain,
∀ j ≤ m,
‖iteratedFDeriv ℝ j (fun (y : D) => f n (e y)) x‖ ≤ WeightedClasses.majorant (ParticularWaveBounds.reindexStrip e s) (fun (k : ℕ) (y : D) => w k (e y)) α C p n
x) ↔ ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f n) x‖ ≤ WeightedClasses.majorant s w α C p n x
The same numerical C,p works on both sides, including all derivatives
up to the supplied order. This is stronger than a fresh existence bound.
theorem
NavierStokes.MeanBoundsReindex.bandBound_pull_iff
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
(s : WeightedClasses.StripData E)
(β : ℝ)
(a : ℕ → ℝ)
:
theorem
NavierStokes.MeanBoundsReindex.meanClass_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{α : ℝ}
{f : MeanIncrementBounds.Field E}
(hf : WeightedClasses.MeanClass s α f)
:
theorem
NavierStokes.MeanBoundsReindex.unweightedClass_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{α : ℝ}
{f : MeanIncrementBounds.Field E}
(hf : WeightedClasses.UnweightedClass s α f)
:
theorem
NavierStokes.MeanBoundsReindex.operatorBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{o : MeanIncrementBounds.Operators E}
{κ : ℝ}
(ho : MeanIncrementBounds.OperatorBounds s o κ)
:
theorem
NavierStokes.MeanBoundsReindex.baseBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{b : MeanIncrementBounds.Triple E}
(hb : MeanIncrementBounds.BaseBounds s b)
:
theorem
NavierStokes.MeanBoundsReindex.meanCumulativeBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{b : MeanIncrementBounds.Triple E}
(hb : MeanIncrementBounds.CumulativeBounds s b)
:
theorem
NavierStokes.MeanBoundsReindex.incrementBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{H : ℝ}
{b : MeanIncrementBounds.Triple E}
(hb : MeanIncrementBounds.IncrementBounds s H b)
:
theorem
NavierStokes.MeanBoundsReindex.context_operatorBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{c : CorrectionState.Context E}
{κ : ℝ}
(ho : MeanIncrementBounds.OperatorBounds s c.operators κ)
:
theorem
NavierStokes.MeanBoundsReindex.context_baseBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{c : CorrectionState.Context E}
(hb : MeanIncrementBounds.BaseBounds s c.base)
:
theorem
NavierStokes.MeanBoundsReindex.cumulativeBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{u : CorrectionState.State E}
(hu : CorrectionState.CumulativeBounds s u)
:
theorem
NavierStokes.MeanBoundsReindex.meanResidualBounds_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{σ : ℝ}
{c : CorrectionState.Context E}
{u : CorrectionState.State E}
(hu : CorrectionState.MeanResidualBounds s σ c u)
:
Returning solver classes to the original chart #
theorem
NavierStokes.MeanBoundsReindex.memClass_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{w : ℕ → D → ℝ}
{α : ℝ}
{f : ℕ → E → F}
(hf : WeightedClasses.MemClass (ParticularWaveBounds.reindexStrip e.symm s) (fun (n : ℕ) (y : E) => w n (e.symm y)) α f)
:
WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n (e x)
theorem
NavierStokes.MeanBoundsReindex.uniformClass_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
{f : ι → ℕ → E → F}
(hf :
LabelSumBounds.UniformClass (ParticularWaveBounds.reindexStrip e.symm s)
(fun (l : ι) (n : ℕ) (y : E) => w l n (e.symm y)) α f)
:
LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => f l n (e x)
Returning a uniform class retains the same constants chosen before both the label and the band.
theorem
NavierStokes.MeanBoundsReindex.context_operatorBounds_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
{κ : ℝ}
(ho :
MeanIncrementBounds.OperatorBounds (ParticularWaveBounds.reindexStrip e.symm s)
(StateReindex.context e.symm c).operators κ)
:
theorem
NavierStokes.MeanBoundsReindex.context_baseBounds_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
(hb : MeanIncrementBounds.BaseBounds (ParticularWaveBounds.reindexStrip e.symm s) (StateReindex.context e.symm c).base)
:
theorem
NavierStokes.MeanBoundsReindex.cumulativeBounds_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{u : CorrectionState.State D}
(hu : CorrectionState.CumulativeBounds (ParticularWaveBounds.reindexStrip e.symm s) (StateReindex.state e.symm u))
:
Uniform classes of the actual harmonic residual #
theorem
NavierStokes.MeanBoundsReindex.residualBlock_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(e : D ≃ₗᵢ[ℝ] E)
(c : CorrectionState.Context D)
(u : CorrectionState.State D)
(b : CorrectionState.HarmonicBlock D)
(G A : HarmonicResidual.BlockCoefficients D)
:
StateReindex.block e
(HarmonicResidual.residualBlock (StateReindex.context e.symm c) (StateReindex.state e.symm u)
(StateReindex.block e.symm b) (StateReindex.blockCoefficients e.symm G)
(StateReindex.blockCoefficients e.symm A)) = HarmonicResidual.residualBlock c u b G A
theorem
NavierStokes.MeanBoundsReindex.uniformVelocity_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_1}
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α : ℝ}
{b : ι → CorrectionState.HarmonicBlock E}
(hb :
UniformHarmonicInteraction.UniformVelocity (ParticularWaveBounds.reindexStrip e.symm s)
(fun (l : ι) (n : ℕ) (y : E) => P l n (e.symm y)) α b)
:
UniformHarmonicInteraction.UniformVelocity s P α fun (l : ι) => StateReindex.block e (b l)
Arbitrary solver block families return with their original common weight and exponent. Uniformity over labels is retained.
theorem
NavierStokes.MeanBoundsReindex.uniformVelocity_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_1}
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{P : ι → ℕ → E → ℝ}
{α : ℝ}
{b : ι → CorrectionState.HarmonicBlock E}
(hb : UniformHarmonicInteraction.UniformVelocity s P α b)
:
UniformHarmonicInteraction.UniformVelocity (ParticularWaveBounds.reindexStrip e s)
(fun (l : ι) (n : ℕ) (x : D) => P l n (e x)) α fun (l : ι) => StateReindex.block e (b l)
theorem
NavierStokes.MeanBoundsReindex.residualBlock_velocity_uniform_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_1}
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{w : ι → ℕ → E → ℝ}
{α : ℝ}
(c : CorrectionState.Context E)
(u : CorrectionState.State E)
(b : ι → CorrectionState.HarmonicBlock E)
(G A : ι → HarmonicResidual.BlockCoefficients E)
(i : Fin 3)
(j : ℤ)
(hb :
LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : E) =>
((HarmonicResidual.residualBlock c u (b l) (G l) (A l)).velocity n i).coeff j x)
:
LabelSumBounds.UniformClass (ParticularWaveBounds.reindexStrip e s) (fun (l : ι) (n : ℕ) (x : D) => w l n (e x)) α
fun (l : ι) (n : ℕ) (x : D) =>
((HarmonicResidual.residualBlock (StateReindex.context e c) (StateReindex.state e u) (StateReindex.block e (b l))
(StateReindex.blockCoefficients e (G l)) (StateReindex.blockCoefficients e (A l))).velocity
n i).coeff
j x
theorem
NavierStokes.MeanBoundsReindex.residualBlock_uniform_pull
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_1}
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData E}
{P : ι → ℕ → E → ℝ}
{α : ℝ}
(c : CorrectionState.Context E)
(u : CorrectionState.State E)
(b : ι → CorrectionState.HarmonicBlock E)
(G A : ι → HarmonicResidual.BlockCoefficients E)
(hb :
UniformHarmonicInteraction.UniformVelocity s P α fun (l : ι) => HarmonicResidual.residualBlock c u (b l) (G l) (A l))
:
UniformHarmonicInteraction.UniformVelocity (ParticularWaveBounds.reindexStrip e s)
(fun (l : ι) (n : ℕ) (x : D) => P l n (e x)) α fun (l : ι) =>
HarmonicResidual.residualBlock (StateReindex.context e c) (StateReindex.state e u) (StateReindex.block e (b l))
(StateReindex.blockCoefficients e (G l)) (StateReindex.blockCoefficients e (A l))
The actual residual is sent to the new chart along with its context, state, carrier and both excluded error coefficient families.
theorem
NavierStokes.MeanBoundsReindex.residualBlock_velocity_uniform_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_1}
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{w : ι → ℕ → D → ℝ}
{α : ℝ}
(c : CorrectionState.Context D)
(u : CorrectionState.State D)
(b : ι → CorrectionState.HarmonicBlock D)
(G A : ι → HarmonicResidual.BlockCoefficients D)
(i : Fin 3)
(j : ℤ)
(hb :
LabelSumBounds.UniformClass (ParticularWaveBounds.reindexStrip e.symm s)
(fun (l : ι) (n : ℕ) (y : E) => w l n (e.symm y)) α fun (l : ι) (n : ℕ) (y : E) =>
((HarmonicResidual.residualBlock (StateReindex.context e.symm c) (StateReindex.state e.symm u)
(StateReindex.block e.symm (b l)) (StateReindex.blockCoefficients e.symm (G l))
(StateReindex.blockCoefficients e.symm (A l))).velocity
n i).coeff
j y)
:
LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) =>
((HarmonicResidual.residualBlock c u (b l) (G l) (A l)).velocity n i).coeff j x
theorem
NavierStokes.MeanBoundsReindex.residualBlock_uniform_return
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ι : Type u_1}
(e : D ≃ₗᵢ[ℝ] E)
{s : WeightedClasses.StripData D}
{P : ι → ℕ → D → ℝ}
{α : ℝ}
(c : CorrectionState.Context D)
(u : CorrectionState.State D)
(b : ι → CorrectionState.HarmonicBlock D)
(G A : ι → HarmonicResidual.BlockCoefficients D)
(hb :
UniformHarmonicInteraction.UniformVelocity (ParticularWaveBounds.reindexStrip e.symm s)
(fun (l : ι) (n : ℕ) (y : E) => P l n (e.symm y)) α fun (l : ι) =>
HarmonicResidual.residualBlock (StateReindex.context e.symm c) (StateReindex.state e.symm u)
(StateReindex.block e.symm (b l)) (StateReindex.blockCoefficients e.symm (G l))
(StateReindex.blockCoefficients e.symm (A l)))
:
UniformHarmonicInteraction.UniformVelocity s P α fun (l : ι) => HarmonicResidual.residualBlock c u (b l) (G l) (A l)
Actual residual classes proved in the associated solver chart return to the original state without an extra operator-bounds hypothesis.
theorem
NavierStokes.MeanBoundsReindex.residualBlock_liftAssoc_uniform_return
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{ι : Type u_1}
{s : WeightedClasses.StripData (PressureStream.Lift S)}
{P : ι → ℕ → PressureStream.Lift S → ℝ}
{α : ℝ}
(c : CorrectionState.Context (PressureStream.Lift S))
(u : CorrectionState.State (PressureStream.Lift S))
(b : ι → CorrectionState.HarmonicBlock (PressureStream.Lift S))
(G A : ι → HarmonicResidual.BlockCoefficients (PressureStream.Lift S))
(hb :
UniformHarmonicInteraction.UniformVelocity
(ParticularWaveBounds.reindexStrip (ParticularWaveBounds.liftAssoc S).symm s)
(fun (l : ι) (n : ℕ) (y : (ℝ × S) × TorusInverse.Plane) => P l n ((ParticularWaveBounds.liftAssoc S).symm y)) α
fun (l : ι) =>
HarmonicResidual.residualBlock (StateReindex.context (ParticularWaveBounds.liftAssoc S).symm c)
(StateReindex.state (ParticularWaveBounds.liftAssoc S).symm u)
(StateReindex.block (ParticularWaveBounds.liftAssoc S).symm (b l))
(StateReindex.blockCoefficients (ParticularWaveBounds.liftAssoc S).symm (G l))
(StateReindex.blockCoefficients (ParticularWaveBounds.liftAssoc S).symm (A l)))
:
UniformHarmonicInteraction.UniformVelocity s P α fun (l : ι) => HarmonicResidual.residualBlock c u (b l) (G l) (A l)
The exact association used by CyclePoint and the particular solver.