Actual moments on the moving profile strip #
The moment map integrates the given fields. It preserves the epsilon exponent using the same moving edge weight. The containing annulus is used only to justify the actual integrals and local smoothness.
theorem
NavierStokes.MovingMomentBounds.radialCoefficient_unweighted
{coord a b cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε L : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hL : ∀ (n : ℕ), 1 ≤ L n)
{q : ℝ → ℝ}
(hq : ContDiff ℝ (↑⊤) q)
:
WeightedClasses.UnweightedClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 0
fun (x : ℕ) (x_1 : LocalSignedRequest.Point) => q x_1.1
A smooth radial multiplier is bounded on the actual moving strip by the compact containing annulus supplied by the positive coordinate range.
theorem
NavierStokes.MovingMomentBounds.pressureMass_mem
{coord a b cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε L : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hL : ∀ (n : ℕ), 1 ≤ L n)
{α : ℝ}
{f : ℕ → LocalSignedRequest.Point → ℝ}
(hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier))
(hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n))
(hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f)
:
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) α fun (n : ℕ) =>
PressureStream.pressureMass (f n)
Actual pressure-mass integration sends the moving mean class to the slow class. The proof bounds the actual jets before integrating them.
theorem
NavierStokes.MovingMomentBounds.radialMoment_mem
{coord a b cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε L : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hL : ∀ (n : ℕ), 1 ≤ L n)
{α : ℝ}
{f : ℕ → LocalSignedRequest.Point → ℝ}
(hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier))
(hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier (f n))
(hclass : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f)
(k : ℕ)
:
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) α
(CorrectionState.radialMoment k f)
def
NavierStokes.MovingMomentBounds.Support
{S : Type}
(a b : ℝ)
(ell : S → ℝ)
(U : Set S)
(f : CorrectionState.ScalarField (PressureStream.Lift S))
:
Support, given by ∀ n, SupportedGauge a b ell U (f n).
Equations
- NavierStokes.MovingMomentBounds.Support a b ell U f = ∀ (n : ℕ), NavierStokes.VariableGaugeMean.SupportedGauge a b ell U (f n)
Instances For
theorem
NavierStokes.MovingMomentBounds.Support.add
{S : Type}
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f g : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hg : Support a b ell U g)
:
theorem
NavierStokes.MovingMomentBounds.Support.neg
{S : Type}
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
:
theorem
NavierStokes.MovingMomentBounds.Support.sub
{S : Type}
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f g : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hg : Support a b ell U g)
:
theorem
NavierStokes.MovingMomentBounds.Support.mul_left
{S : Type}
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(g : CorrectionState.ScalarField (PressureStream.Lift S))
:
theorem
NavierStokes.MovingMomentBounds.Support.mul_right
{S : Type}
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(g : CorrectionState.ScalarField (PressureStream.Lift S))
:
theorem
NavierStokes.MovingMomentBounds.Support.smul
{S : Type}
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(r : ℝ)
:
theorem
NavierStokes.MovingMomentBounds.Support.directional
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hU : IsOpen U)
(hl : ContinuousOn ell U)
(v : PressureStream.Lift S)
:
Support a b ell U fun (n : ℕ) (x : PressureStream.Lift S) => (fderiv ℝ (f n) x) v
theorem
NavierStokes.MovingMomentBounds.Support.dr
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hU : IsOpen U)
(hl : ContinuousOn ell U)
(o : MeanIncrementBounds.Operators (PressureStream.Lift S))
:
theorem
NavierStokes.MovingMomentBounds.Support.dz
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hU : IsOpen U)
(hl : ContinuousOn ell U)
(o : MeanIncrementBounds.Operators (PressureStream.Lift S))
:
theorem
NavierStokes.MovingMomentBounds.Support.time
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hU : IsOpen U)
(hl : ContinuousOn ell U)
(o : MeanIncrementBounds.Operators (PressureStream.Lift S))
:
theorem
NavierStokes.MovingMomentBounds.Support.radialDiv
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hU : IsOpen U)
(hl : ContinuousOn ell U)
(o : MeanIncrementBounds.Operators (PressureStream.Lift S))
(r : ℝ)
:
theorem
NavierStokes.MovingMomentBounds.Support.viscosity
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{f : CorrectionState.ScalarField (PressureStream.Lift S)}
(hf : Support a b ell U f)
(hU : IsOpen U)
(hl : ContinuousOn ell U)
(o : MeanIncrementBounds.Operators (PressureStream.Lift S))
(r : ℝ)
:
structure
NavierStokes.MovingMomentBounds.SupportedTriple
{S : Type}
(a b : ℝ)
(ell : S → ℝ)
(U : Set S)
(m : MeanIncrementBounds.Triple (PressureStream.Lift S))
:
Supported triple data, collecting radial, angular, axial.
Instances For
theorem
NavierStokes.MovingMomentBounds.SupportedTriple.updated
{S : Type}
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
{m h : MeanIncrementBounds.Triple (PressureStream.Lift S)}
(hm : SupportedTriple a b ell U m)
(hh : SupportedTriple a b ell U h)
:
SupportedTriple a b ell U (MeanIncrementBounds.updated m h)
theorem
NavierStokes.MovingMomentBounds.gr_support
{S : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
{a b : ℝ}
{ell : S → ℝ}
{U : Set S}
(hU : IsOpen U)
(hl : ContinuousOn ell U)
(o : MeanIncrementBounds.Operators (PressureStream.Lift S))
(base m : MeanIncrementBounds.Triple (PressureStream.Lift S))
(W : Fin 3 → Fin 3 → CorrectionState.ScalarField (PressureStream.Lift S))
(hm : SupportedTriple a b ell U m)
(hW : ∀ (i j : Fin 3), Support a b ell U (W i j))
:
Support a b ell U (MeanIncrementBounds.gr o base m W)
theorem
NavierStokes.MovingMomentBounds.remainders_mem
{coord a b cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε L : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hL : ∀ (n : ℕ), 1 ≤ L n)
{o : MeanIncrementBounds.Operators LocalSignedRequest.Point}
{base m h : MeanIncrementBounds.Triple LocalSignedRequest.Point}
{κ H : ℝ}
(hop : LocalRankDefect.LocalOperators U.carrier o)
(hbs : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) base)
(hmc : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) m)
(hhc : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) h)
(hms : SupportedTriple a b (VariableGaugeMean.qLength coord) U.carrier m)
(hhs : SupportedTriple a b (VariableGaugeMean.qLength coord) U.carrier h)
(W : Fin 3 → Fin 3 → CorrectionState.ScalarField LocalSignedRequest.Point)
(hWc : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) (W i j))
(hWs : ∀ (i j : Fin 3), Support a b (VariableGaugeMean.qLength coord) U.carrier (W i j))
(ho :
MeanIncrementBounds.OperatorBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) o κ)
(hb : MeanIncrementBounds.BaseBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) base)
(hm :
MeanIncrementBounds.CumulativeBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) m)
(hh :
MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H h)
(hH : 9 / 10 ≤ H)
(i : Fin 3)
:
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (H + 9 / 10 - 2 * κ)
fun (n : ℕ) (x : LocalSignedRequest.Plane) => DefectIncrementBounds.remainders o base m h W n x i
Actual equation-(32) remainders gain their full exponent under the moving moment map. Every covariance and differentiated mean term remains in the source before integration.
theorem
NavierStokes.MovingMomentBounds.rankStage_defect_class
{coord cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData PressureStream.Plane)
(r : CorrectionState.RankData PressureStream.Plane)
(ha : 0 < g.radial.inner)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε L : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hL : ∀ (n : ℕ), 1 ≤ L n)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(axial : PressureStream.Plane × PressureStream.Plane)
(c : CorrectionState.Context LocalSignedRequest.Point)
(u : CorrectionState.State LocalSignedRequest.Point)
(hg : LocalRankDefect.RankGeometry g r U.carrier c u)
{κ H : ℝ}
(hop : LocalRankDefect.LocalOperators U.carrier c.operators)
(hbc : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base)
(hmc : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) u.mean)
(hms : SupportedTriple g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier u.mean)
(hWc : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) (u.covariance i j))
(hWs :
∀ (i j : Fin 3), Support g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j))
(hV : LocalRankDefect.IsSlowOn U.carrier c.base.angular)
(hG : LocalRankDefect.IsSlowOn U.carrier c.base.axial)
(ho :
MeanIncrementBounds.OperatorBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.operators κ)
(hb :
MeanIncrementBounds.BaseBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.base)
(hm :
MeanIncrementBounds.CumulativeBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) u.mean)
(hi :
MeanIncrementBounds.IncrementBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H
(VariableGaugeMean.rankIncrementState g r axial c u))
(hH : 9 / 10 ≤ H)
(i : Fin 3)
:
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) (H + 9 / 10 - 2 * κ)
fun (n : ℕ) (x : LocalSignedRequest.Plane) =>
CorrectionState.debt c (VariableGaugeMean.rankStageState g r axial c u) n x i
The actual five-row rank stage gains the defect exponent on the original moving strip. The row cancellation is derived from RankGeometry; the pressure source and quadratic remainders are integrated literally.
theorem
NavierStokes.MovingMomentBounds.rankStage_defectBounds
{coord cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData PressureStream.Plane)
(r : CorrectionState.RankData PressureStream.Plane)
(ha : 0 < g.radial.inner)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε L : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hL : ∀ (n : ℕ), 1 ≤ L n)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(axial : PressureStream.Plane × PressureStream.Plane)
(c : CorrectionState.Context LocalSignedRequest.Point)
(u : CorrectionState.State LocalSignedRequest.Point)
(hg : LocalRankDefect.RankGeometry g r U.carrier c u)
{κ H σ : ℝ}
(hop : LocalRankDefect.LocalOperators U.carrier c.operators)
(hbc : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain U.carrier) c.base)
(hmc : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain U.carrier) u.mean)
(hms : SupportedTriple g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier u.mean)
(hWc : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U.carrier) (u.covariance i j))
(hWs :
∀ (i j : Fin 3), Support g.radial.inner g.radial.outer (VariableGaugeMean.qLength coord) U.carrier (u.covariance i j))
(hV : LocalRankDefect.IsSlowOn U.carrier c.base.angular)
(hG : LocalRankDefect.IsSlowOn U.carrier c.base.axial)
(ho :
MeanIncrementBounds.OperatorBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.operators κ)
(hb :
MeanIncrementBounds.BaseBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) c.base)
(hm :
MeanIncrementBounds.CumulativeBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) u.mean)
(hi :
MeanIncrementBounds.IncrementBounds
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H
(VariableGaugeMean.rankIncrementState g r axial c u))
(hH : 9 / 10 ≤ H)
(hσ : 1 + σ ≤ H + 9 / 10 - 2 * κ)
:
CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) σ c
(VariableGaugeMean.rankStageState g r axial c u)