Rank correction on the actual open slow domain #
The stream uses the variable similarity gauge. Its zero weighted mass makes it equal to the same zero-axis primitive in every containing gauge. All moment estimates below use the local physical domain, not global slow data.
@[reducible, inline]
Point: an abbreviation for PressureStream.Lift P.
Instances For
Positive domain, given by DefectIncrementBounds.positiveDomain ∩ PhysicalMeanDomain.slowDomain U.
Equations
Instances For
theorem
NavierStokes.LocalRankDefect.positiveDomain_open
{P : Type}
[NormedAddCommGroup P]
{U : Set P}
(hU : IsOpen U)
:
IsOpen (positiveDomain U)
structure
NavierStokes.LocalRankDefect.LocalShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(a b : ℝ)
(U : Set P)
(f : ScalarField (Point P))
:
Smoothness and radial support only where the slow parameter is used.
- smooth : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain U) f
- supported (n : ℕ) : PhysicalMeanDomain.SupportedOn a b U (f n)
Instances For
theorem
NavierStokes.LocalRankDefect.LocalShell.zero_of_not_mem
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(n : ℕ)
(x : Point P)
(hx : x.2.1 ∈ U)
(hr : x.1 ∉ Set.Icc a b)
:
theorem
NavierStokes.LocalRankDefect.LocalShell.zero
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
:
LocalShell a b U 0
theorem
NavierStokes.LocalRankDefect.LocalShell.add
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f g : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hg : LocalShell a b U g)
:
LocalShell a b U (f + g)
theorem
NavierStokes.LocalRankDefect.LocalShell.neg
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
:
LocalShell a b U (-f)
theorem
NavierStokes.LocalRankDefect.LocalShell.sub
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f g : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hg : LocalShell a b U g)
:
LocalShell a b U (f - g)
theorem
NavierStokes.LocalRankDefect.LocalShell.mul
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f g : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hg : LocalShell a b U g)
:
LocalShell a b U (f * g)
theorem
NavierStokes.LocalRankDefect.LocalShell.band_mul
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(c : ℕ → ℝ)
:
LocalShell a b U fun (n : ℕ) (x : Point P) => c n * f n x
theorem
NavierStokes.LocalRankDefect.LocalShell.smul
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(c : ℝ)
:
LocalShell a b U (c • f)
theorem
NavierStokes.LocalRankDefect.LocalShell.directional
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hU : IsOpen U)
(v : Point P)
:
LocalShell a b U fun (n : ℕ) (x : Point P) => (fderiv ℝ (f n) x) v
theorem
NavierStokes.LocalRankDefect.LocalShell.coefficient_mul
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f g : ScalarField (Point P)}
(hf : LocalShell a b U f)
(ha : 0 < a)
(hU : IsOpen U)
(hg : MeanIncrementBounds.SmoothOn (positiveDomain U) g)
:
LocalShell a b U (g * f)
theorem
NavierStokes.LocalRankDefect.LocalShell.mul_coefficient
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f g : ScalarField (Point P)}
(hf : LocalShell a b U f)
(ha : 0 < a)
(hU : IsOpen U)
(hg : MeanIncrementBounds.SmoothOn (positiveDomain U) g)
:
LocalShell a b U (f * g)
theorem
NavierStokes.LocalRankDefect.LocalShell.freeze
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hU : IsOpen U)
{x : P}
(hx : x ∈ U)
:
DefectIncrementBounds.Shell a b fun (n : ℕ) => PhysicalMeanDomain.freezeSlow x (f n)
structure
NavierStokes.LocalRankDefect.LocalTriple
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(a b : ℝ)
(U : Set P)
(m : MeanIncrementBounds.Triple (Point P))
:
Local triple data, collecting radial, angular, axial.
- radial : LocalShell a b U m.radial
- angular : LocalShell a b U m.angular
- axial : LocalShell a b U m.axial
Instances For
theorem
NavierStokes.LocalRankDefect.LocalTriple.updated
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{m h : MeanIncrementBounds.Triple (Point P)}
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
:
LocalTriple a b U (MeanIncrementBounds.updated m h)
theorem
NavierStokes.LocalRankDefect.LocalTriple.smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{m : MeanIncrementBounds.Triple (Point P)}
(hm : LocalTriple a b U m)
:
structure
NavierStokes.LocalRankDefect.LocalOperators
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(U : Set P)
(o : MeanIncrementBounds.Operators (Point P))
:
Local operators data, collecting radius_eq, radialProfile.
- radialProfile : ContDiffOn ℝ (↑⊤) o.radialProfile (positiveDomain U)
Instances For
theorem
NavierStokes.LocalRankDefect.LocalOperators.invRadius_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{U : Set P}
{o : MeanIncrementBounds.Operators (Point P)}
(ho : LocalOperators U o)
:
theorem
NavierStokes.LocalRankDefect.LocalShell.dr
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
{o : MeanIncrementBounds.Operators (Point P)}
(hf : LocalShell a b U f)
(ha : 0 < a)
(hU : IsOpen U)
(ho : LocalOperators U o)
:
LocalShell a b U (o.dr f)
theorem
NavierStokes.LocalRankDefect.LocalShell.dz
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hU : IsOpen U)
(o : MeanIncrementBounds.Operators (Point P))
:
LocalShell a b U (o.dz f)
theorem
NavierStokes.LocalRankDefect.LocalShell.time
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hU : IsOpen U)
(o : MeanIncrementBounds.Operators (Point P))
:
LocalShell a b U (o.time f)
theorem
NavierStokes.LocalRankDefect.LocalShell.inv_mul
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
{o : MeanIncrementBounds.Operators (Point P)}
(hf : LocalShell a b U f)
(ha : 0 < a)
(hU : IsOpen U)
(ho : LocalOperators U o)
:
LocalShell a b U (o.invRadius * f)
theorem
NavierStokes.LocalRankDefect.LocalShell.radialDiv
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
{o : MeanIncrementBounds.Operators (Point P)}
(hf : LocalShell a b U f)
(ha : 0 < a)
(hU : IsOpen U)
(ho : LocalOperators U o)
(c : ℝ)
:
LocalShell a b U (o.radialDiv c f)
theorem
NavierStokes.LocalRankDefect.LocalShell.viscosity
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
{o : MeanIncrementBounds.Operators (Point P)}
(hf : LocalShell a b U f)
(ha : 0 < a)
(hU : IsOpen U)
(ho : LocalOperators U o)
(c : ℝ)
:
LocalShell a b U (o.viscosity c f)
theorem
NavierStokes.LocalRankDefect.thetaAxial_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
:
LocalShell a b U (MeanIncrementBounds.thetaAxial base m)
theorem
NavierStokes.LocalRankDefect.axialAxial_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
:
LocalShell a b U (MeanIncrementBounds.axialAxial base m)
theorem
NavierStokes.LocalRankDefect.axialRadial_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
:
LocalShell a b U (MeanIncrementBounds.axialRadial base m)
theorem
NavierStokes.LocalRankDefect.radialRadial_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
:
LocalShell a b U (MeanIncrementBounds.radialRadial base m)
theorem
NavierStokes.LocalRankDefect.radialAngular_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
:
LocalShell a b U (MeanIncrementBounds.radialAngular base m)
theorem
NavierStokes.LocalRankDefect.gr_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
{o : MeanIncrementBounds.Operators (Point P)}
(ho : LocalOperators U o)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
:
LocalShell a b U (MeanIncrementBounds.gr o base m W)
theorem
NavierStokes.LocalRankDefect.leadingRadial_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hh : LocalTriple a b U h)
{o : MeanIncrementBounds.Operators (Point P)}
(ho : LocalOperators U o)
:
LocalShell a b U (MeanIncrementBounds.leadingRadial o base h)
theorem
NavierStokes.LocalRankDefect.thetaQuadratic_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{m h : MeanIncrementBounds.Triple (Point P)}
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
:
LocalShell a b U (DefectIncrementBounds.thetaQuadratic m h)
theorem
NavierStokes.LocalRankDefect.axialQuadratic_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{m h : MeanIncrementBounds.Triple (Point P)}
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
:
LocalShell a b U (DefectIncrementBounds.axialQuadratic m h)
theorem
NavierStokes.LocalRankDefect.thetaLeading_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hh : LocalTriple a b U h)
:
LocalShell a b U (DefectIncrementBounds.thetaLeading base h)
theorem
NavierStokes.LocalRankDefect.axialLeading_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hh : LocalTriple a b U h)
:
LocalShell a b U (DefectIncrementBounds.axialLeading base h)
theorem
NavierStokes.LocalRankDefect.actualRadialError_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
{o : MeanIncrementBounds.Operators (Point P)}
(ho : LocalOperators U o)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
:
LocalShell a b U (DefectIncrementBounds.actualRadialError o base m h W)
theorem
NavierStokes.LocalRankDefect.LocalShell.barIntegrable
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hU : IsOpen U)
(k n : ℕ)
{p : P}
(hp : p ∈ U)
:
MeasureTheory.Integrable (fun (r : ℝ) => r ^ k * PressureStream.torusAverage (f n) (r, p)) MeasureTheory.volume
theorem
NavierStokes.LocalRankDefect.LocalShell.sliceIntegrable
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hU : IsOpen U)
(k n : ℕ)
{p : P}
(hp : p ∈ U)
:
MeasureTheory.Integrable (fun (r : ℝ) => r ^ k * DefectIncrementBounds.slowSlice f n p r) MeasureTheory.volume
theorem
NavierStokes.LocalRankDefect.barMoment_add_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
(hU : IsOpen U)
{f g : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hg : LocalShell a b U g)
(k n : ℕ)
{p : P}
(hp : p ∈ U)
:
DefectIncrementBounds.barMoment k (f + g) n p = DefectIncrementBounds.barMoment k f n p + DefectIncrementBounds.barMoment k g n p
theorem
NavierStokes.LocalRankDefect.barMoment_sub_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{U : Set P}
(hU : IsOpen U)
{f g : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hg : LocalShell a b U g)
(k n : ℕ)
{p : P}
(hp : p ∈ U)
:
DefectIncrementBounds.barMoment k (f - g) n p = DefectIncrementBounds.barMoment k f n p - DefectIncrementBounds.barMoment k g n p
theorem
NavierStokes.LocalRankDefect.barMoment_mem_local
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{a b cL cR : ℝ}
(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)
(U : Set P)
(hU : IsOpen U)
{α : ℝ}
{f : ScalarField (Point P)}
(hf : LocalShell a b U f)
(hclass : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f)
(k : ℕ)
:
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U hU ε L hε hεone hL) α
(DefectIncrementBounds.barMoment k f)
theorem
NavierStokes.LocalRankDefect.pressureDefect_update_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{o : MeanIncrementBounds.Operators (Point P)}
(hop : LocalOperators U o)
{base m h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
(n : ℕ)
{p : P}
(hp : p ∈ U)
:
DefectIncrementBounds.pressureDefect o base (MeanIncrementBounds.updated m h) W n p = DefectIncrementBounds.pressureDefect o base m W n p + DefectIncrementBounds.barMoment 0 (MeanIncrementBounds.leadingRadial o base h) n p + DefectIncrementBounds.barMoment 0 (DefectIncrementBounds.actualRadialError o base m h W) n p
theorem
NavierStokes.LocalRankDefect.thetaDefect_update_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{base m h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
(n : ℕ)
{p : P}
(hp : p ∈ U)
:
DefectIncrementBounds.thetaDefect base (MeanIncrementBounds.updated m h) W n p = DefectIncrementBounds.thetaDefect base m W n p + DefectIncrementBounds.barMoment 2 (DefectIncrementBounds.thetaLeading base h) n p + DefectIncrementBounds.barMoment 2 (DefectIncrementBounds.thetaQuadratic m h) n p
theorem
NavierStokes.LocalRankDefect.axialDefect_update_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{o : MeanIncrementBounds.Operators (Point P)}
(hop : LocalOperators U o)
{base m h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
(n : ℕ)
{p : P}
(hp : p ∈ U)
:
DefectIncrementBounds.axialDefect o base (MeanIncrementBounds.updated m h) W n p = DefectIncrementBounds.axialDefect o base m W n p + (DefectIncrementBounds.barMoment 1 (DefectIncrementBounds.axialLeading base h) n p - 1 / 2 * DefectIncrementBounds.barMoment 2 (MeanIncrementBounds.leadingRadial o base h) n p) + (DefectIncrementBounds.barMoment 1 (DefectIncrementBounds.axialQuadratic m h) n p - 1 / 2 * DefectIncrementBounds.barMoment 2 (DefectIncrementBounds.actualRadialError o base m h W) n p)
theorem
NavierStokes.LocalRankDefect.defects_update_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{o : MeanIncrementBounds.Operators (Point P)}
(hop : LocalOperators U o)
{base m h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
(n : ℕ)
{p : P}
(hp : p ∈ U)
:
DefectIncrementBounds.defects o base (MeanIncrementBounds.updated m h) W n p = DefectIncrementBounds.defects o base m W n p + DefectIncrementBounds.linearRows o base h n p + DefectIncrementBounds.remainders o base m h W n p
theorem
NavierStokes.LocalRankDefect.defects_after_solved_rows_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{o : MeanIncrementBounds.Operators (Point P)}
(hop : LocalOperators U o)
{base m h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hm : LocalTriple a b U m)
(hh : LocalTriple a b U h)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
(n : ℕ)
{p : P}
(hp : p ∈ U)
(hrows : DefectIncrementBounds.linearRows o base h n p = -DefectIncrementBounds.defects o base m W n p)
:
DefectIncrementBounds.defects o base (MeanIncrementBounds.updated m h) W n p = DefectIncrementBounds.remainders o base m h W n p
theorem
NavierStokes.LocalRankDefect.remainders_mem_local
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{a b cL cR : ℝ}
(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)
(U : Set P)
(hU : IsOpen U)
{o : MeanIncrementBounds.Operators (Point P)}
{κ H : ℝ}
{base m h : MeanIncrementBounds.Triple (Point P)}
(hop : LocalOperators U o)
(hbs : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hms : LocalTriple a b U m)
(hhs : LocalTriple a b U h)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(hW : ∀ (i j : Fin 3), LocalShell a b U (W i j))
(ho :
MeanIncrementBounds.OperatorBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) o κ)
(hb : MeanIncrementBounds.BaseBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) base)
(hm :
MeanIncrementBounds.CumulativeBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) m)
(hh :
MeanIncrementBounds.IncrementBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H h)
(hH : 9 / 10 ≤ H)
(i : Fin 3)
:
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U hU ε L hε hεone hL) (H + 9 / 10 - 2 * κ)
fun (n : ℕ) (p : P) => DefectIncrementBounds.remainders o base m h W n p i
Integration uses actual local moments; the complete equation-(32) remainder is derived before integration.
noncomputable def
NavierStokes.LocalRankDefect.IsSlowOn
{P : Type}
(U : Set P)
(f : ScalarField (Point P))
:
Is slow on, given by ∀ n R p, p ∈ U → ∀ Y, f n (R, (p, Y)) = slowSlice f n p R.
Equations
- NavierStokes.LocalRankDefect.IsSlowOn U f = ∀ (n : ℕ) (R : ℝ), ∀ p ∈ U, ∀ (Y : NavierStokes.PressureStream.Plane), f n (R, p, Y) = NavierStokes.DefectIncrementBounds.slowSlice f n p R
Instances For
theorem
NavierStokes.LocalRankDefect.IsSlowOn.add
{P : Type}
{U : Set P}
{f g : ScalarField (Point P)}
(hf : IsSlowOn U f)
(hg : IsSlowOn U g)
:
theorem
NavierStokes.LocalRankDefect.IsSlowOn.mul
{P : Type}
{U : Set P}
{f g : ScalarField (Point P)}
(hf : IsSlowOn U f)
(hg : IsSlowOn U g)
:
theorem
NavierStokes.LocalRankDefect.IsSlowOn.smul
{P : Type}
{U : Set P}
{f : ScalarField (Point P)}
(hf : IsSlowOn U f)
(c : ℝ)
:
theorem
NavierStokes.LocalRankDefect.LocalOperators.invRadius_slow
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{U : Set P}
{o : MeanIncrementBounds.Operators (Point P)}
(ho : LocalOperators U o)
:
theorem
NavierStokes.LocalRankDefect.barMoment_slow_on
{P : Type}
{U : Set P}
{f : ScalarField (Point P)}
(hf : IsSlowOn U f)
(k n : ℕ)
{p : P}
(hp : p ∈ U)
:
DefectIncrementBounds.barMoment k f n p = ∫ (R : ℝ), R ^ k * DefectIncrementBounds.slowSlice f n p R
theorem
NavierStokes.LocalRankDefect.linearRows_eq_neg_of_fiveRows_on
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
(ha : 0 < a)
{U : Set P}
(hU : IsOpen U)
{o : MeanIncrementBounds.Operators (Point P)}
(hop : LocalOperators U o)
{base m h : MeanIncrementBounds.Triple (Point P)}
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) base)
(hh : LocalTriple a b U h)
(hV : IsSlowOn U base.angular)
(hG : IsSlowOn U base.axial)
(hv : IsSlowOn U h.angular)
(hg : IsSlowOn U h.axial)
(W : Fin 3 → Fin 3 → ScalarField (Point P))
(n : ℕ)
{p : P}
(hp : p ∈ U)
(hrows :
FiveRowRank.FiveRows (DefectIncrementBounds.slowSlice base.angular n p)
(DefectIncrementBounds.slowSlice base.axial n p) (DefectIncrementBounds.defects o base m W n p)
(DefectIncrementBounds.slowSlice h.angular n p) (DefectIncrementBounds.slowSlice h.axial n p))
:
The constructed rank source and the variable gauge #
theorem
NavierStokes.LocalRankDefect.gauge_streamPotential_eq_fixed
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(d a b M : ℝ)
(ell : P → ℝ)
(v : PressureStream.Plane)
(f : Point P → ℝ)
(p : Point P)
:
VariableGaugeMean.streamPotential d a b M ell v f p = PressureStream.streamPotential d (ell p.2.1 * a) (ell p.2.1 * b) M (0, v) f p
theorem
NavierStokes.LocalRankDefect.slow_gaugePotential_eq_scaledPrimitive
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b d M : ℝ}
(ha : 0 < a)
(hab : a < b)
(hd : 0 < d)
(ell : P → ℝ)
(v : PressureStream.Plane)
(f : ℝ × P → ℝ)
(p : Point P)
(hl : 0 < ell p.2.1)
(hf : ContDiff ℝ ↑⊤ fun (R : ℝ) => f (R, p.2.1))
(hs : (Function.support fun (R : ℝ) => f (R, p.2.1)) ⊆ Set.Icc (ell p.2.1 * a) (ell p.2.1 * b))
(hm : ∫ (R : ℝ), R * f (R, p.2.1) = 0)
:
VariableGaugeMean.streamPotential d a b M ell v (MeanRankUpdate.slowLift f) p = MeanRankUpdate.scaledPrimitive (fun (R : ℝ) => f (R, p.2.1)) p.1
A zero-mass slow source removes the actual variable gauge cutoff.
theorem
NavierStokes.LocalRankDefect.rankDesired_slice_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(r : CorrectionState.RankData P)
(c : CorrectionState.Context (Point P))
(u : CorrectionState.State (Point P))
(n : ℕ)
(x : P)
:
structure
NavierStokes.LocalRankDefect.RankGeometry
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(g : VariableGaugeMean.GaugeData P)
(r : CorrectionState.RankData P)
(U : Set P)
(c : CorrectionState.Context (Point P))
(u : CorrectionState.State (Point P))
:
Primitive rank data and the actual base patch model, restricted to the open physical slow domain. Invertibility, masses, and rows are conclusions.
- coefficient_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (r.coefficient n) U
- length_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (r.length n) U
- velocity_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (r.velocity n) U
- debt_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (CorrectionState.debt c u n) U
Instances For
theorem
NavierStokes.LocalRankDefect.RankGeometry.angular_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (CorrectionState.rankAngular r c u n) (Set.univ ×ˢ U)
theorem
NavierStokes.LocalRankDefect.RankGeometry.desired_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (CorrectionState.rankDesiredAxial r c u n) (Set.univ ×ˢ U)
theorem
NavierStokes.LocalRankDefect.RankGeometry.angular_lift_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (MeanRankUpdate.slowLift (CorrectionState.rankAngular r c u n)) (PhysicalMeanDomain.slowDomain U)
theorem
NavierStokes.LocalRankDefect.RankGeometry.desired_lift_smooth
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n)) (PhysicalMeanDomain.slowDomain U)
theorem
NavierStokes.LocalRankDefect.RankGeometry.desired_slice_support
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
{x : P}
(hx : x ∈ U)
{lo hi : ℝ}
(hlo : lo ≤ r.length n x * r.inner)
(hhi : r.length n x * r.outer ≤ hi)
:
(Function.support fun (R : ℝ) => CorrectionState.rankDesiredAxial r c u n (R, x)) ⊆ Set.Icc lo hi
theorem
NavierStokes.LocalRankDefect.RankGeometry.desired_supported
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(n : ℕ)
:
theorem
NavierStokes.LocalRankDefect.RankGeometry.angular_supported
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(n : ℕ)
:
PhysicalMeanDomain.SupportedOn a b U (MeanRankUpdate.slowLift (CorrectionState.rankAngular r c u n))
theorem
NavierStokes.LocalRankDefect.RankGeometry.desired_mass_zero
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
{x : P}
(hx : x ∈ U)
:
theorem
NavierStokes.LocalRankDefect.RankGeometry.potential_eq_scaledPrimitive
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
{p : Point P}
(hp : p.2.1 ∈ U)
:
VariableGaugeMean.rankPotential g r c u n p = MeanRankUpdate.scaledPrimitive (fun (R : ℝ) => CorrectionState.rankDesiredAxial r c u n (R, p.2.1)) p.1
theorem
NavierStokes.LocalRankDefect.RankGeometry.potential_eq_fixed
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(n : ℕ)
{p : Point P}
(hp : p.2.1 ∈ U)
:
VariableGaugeMean.rankPotential g r c u n p = PressureStream.streamPotential g.radial.exponent a b (g.radial.frequency n) (0, g.radial.radialDirection)
(MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n)) p
theorem
NavierStokes.LocalRankDefect.RankGeometry.potential_eventuallyEq_fixed
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(n : ℕ)
{p : Point P}
(hp : p.2.1 ∈ U)
:
VariableGaugeMean.rankPotential g r c u n =ᶠ[nhds p] PressureStream.streamPotential g.radial.exponent a b (g.radial.frequency n) (0, g.radial.radialDirection)
(MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n))
theorem
NavierStokes.LocalRankDefect.RankGeometry.potential_localShell
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
[FiniteDimensional ℝ P]
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
:
LocalShell a b U (VariableGaugeMean.rankPotential g r c u)
theorem
NavierStokes.LocalRankDefect.RankGeometry.axial_exact
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
[FiniteDimensional ℝ P]
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
(n : ℕ)
{p : Point P}
(hp : p.2.1 ∈ U)
:
(VariableGaugeMean.rankIncrementState g r axial c u).axial n p = CorrectionState.rankDesiredAxial r c u n (p.1, p.2.1)
The actual variable-gauge axial stream is the desired rank source.
theorem
NavierStokes.LocalRankDefect.streamBeta_smul
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(a : ℝ)
(w : P × PressureStream.Plane)
(F : Point P → ℝ)
:
PressureStream.streamBeta (a • w) F = fun (p : ℝ × P × PressureStream.Plane) => a * PressureStream.streamBeta w F p
theorem
NavierStokes.LocalRankDefect.rankStage_covariance
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(g : VariableGaugeMean.GaugeData P)
(r : CorrectionState.RankData P)
(axial : P × PressureStream.Plane)
(c : CorrectionState.Context (Point P))
(u : CorrectionState.State (Point P))
:
theorem
NavierStokes.LocalRankDefect.rankStage_debt_eq
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(g : VariableGaugeMean.GaugeData P)
(r : CorrectionState.RankData P)
(axial : P × PressureStream.Plane)
(c : CorrectionState.Context (Point P))
(u : CorrectionState.State (Point P))
:
CorrectionState.debt c (VariableGaugeMean.rankStageState g r axial c u) = DefectIncrementBounds.defects c.operators c.base
(MeanIncrementBounds.updated u.mean (VariableGaugeMean.rankIncrementState g r axial c u)) u.covariance
theorem
NavierStokes.LocalRankDefect.rank_angular_slow
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
(g : VariableGaugeMean.GaugeData P)
(r : CorrectionState.RankData P)
(axial : P × PressureStream.Plane)
(U : Set P)
(c : CorrectionState.Context (Point P))
(u : CorrectionState.State (Point P))
:
IsSlowOn U (VariableGaugeMean.rankIncrementState g r axial c u).angular
theorem
NavierStokes.LocalRankDefect.RankGeometry.increment_localTriple
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
:
LocalTriple a b U (VariableGaugeMean.rankIncrementState g r axial c u)
theorem
NavierStokes.LocalRankDefect.RankGeometry.axial_slow
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
:
IsSlowOn U (VariableGaugeMean.rankIncrementState g r axial c u).axial
theorem
NavierStokes.LocalRankDefect.RankGeometry.divergence_zero
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
(n : ℕ)
{p : Point P}
(hp : p.2.1 ∈ U)
(hr : p.1 ≠ 0)
:
PressureStream.graphDivergence (PressureStream.physicalSpeed g.radial.exponent (g.radial.frequency n))
(0, g.radial.radialDirection) (c.operators.epsilon n • axial)
((VariableGaugeMean.rankIncrementState g r axial c u).radial n)
((VariableGaugeMean.rankIncrementState g r axial c u).axial n) p = 0
theorem
NavierStokes.LocalRankDefect.RankGeometry.fiveRows
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
(n : ℕ)
{x : P}
(hx : x ∈ U)
:
FiveRowRank.FiveRows (DefectIncrementBounds.slowSlice c.base.angular n x)
(DefectIncrementBounds.slowSlice c.base.axial n x) (CorrectionState.debt c u n x)
(DefectIncrementBounds.slowSlice (VariableGaugeMean.rankIncrementState g r axial c u).angular n x)
(DefectIncrementBounds.slowSlice (VariableGaugeMean.rankIncrementState g r axial c u).axial n x)
theorem
NavierStokes.LocalRankDefect.RankGeometry.solved_rows
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
(hop : LocalOperators U c.operators)
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) c.base)
(hV : IsSlowOn U c.base.angular)
(hG : IsSlowOn U c.base.axial)
(n : ℕ)
{x : P}
(hx : x ∈ U)
:
DefectIncrementBounds.linearRows c.operators c.base (VariableGaugeMean.rankIncrementState g r axial c u) n x = -CorrectionState.debt c u n x
theorem
NavierStokes.LocalRankDefect.RankGeometry.preserve_masses
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
(hm : LocalTriple a b U u.mean)
(n : ℕ)
{x : P}
(hx : x ∈ U)
:
CorrectionState.radialMoment 2 (VariableGaugeMean.rankStageState g r axial c u).mean.angular n x = CorrectionState.radialMoment 2 u.mean.angular n x ∧ CorrectionState.radialMoment 1 (VariableGaugeMean.rankStageState g r axial c u).mean.axial n x = CorrectionState.radialMoment 1 u.mean.axial n x
theorem
NavierStokes.LocalRankDefect.RankGeometry.debt_eq_remainders
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
(hop : LocalOperators U c.operators)
(hb : MeanIncrementBounds.SmoothTriple (positiveDomain U) c.base)
(hm : LocalTriple a b U u.mean)
(hW : ∀ (i j : Fin 3), LocalShell a b U (u.covariance i j))
(hV : IsSlowOn U c.base.angular)
(hG : IsSlowOn U c.base.axial)
(n : ℕ)
{x : P}
(hx : x ∈ U)
:
CorrectionState.debt c (VariableGaugeMean.rankStageState g r axial c u) n x = DefectIncrementBounds.remainders c.operators c.base u.mean (VariableGaugeMean.rankIncrementState g r axial c u)
u.covariance n x
theorem
NavierStokes.LocalRankDefect.RankGeometry.potential_class
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{a b cL cR : ℝ}
(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)
(U : Set P)
(hU : IsOpen U)
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
{H : ℝ}
(hsource :
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n))
:
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
(VariableGaugeMean.rankPotential g r c u)
theorem
NavierStokes.LocalRankDefect.RankGeometry.increment_bounds
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{a b cL cR : ℝ}
(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)
(U : Set P)
(hU : IsOpen U)
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
{H : ℝ}
(hangular :
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankAngular r c u n))
(haxial :
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n))
(heps :
WeightedClasses.BandBound (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) 1
c.operators.epsilon)
:
MeanIncrementBounds.IncrementBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
(VariableGaugeMean.rankIncrementState g r axial c u)
The extra epsilon in the actual radial stream yields M_(H+1).
Both source classes refer to the already constructed rank inverse.
theorem
NavierStokes.LocalRankDefect.rankStage_defect_class
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{a b cL cR : ℝ}
(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)
(U : Set P)
(hU : IsOpen U)
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
{H κ : ℝ}
(hop : LocalOperators U c.operators)
(hbs : MeanIncrementBounds.SmoothTriple (positiveDomain U) c.base)
(hms : LocalTriple a b U u.mean)
(hW : ∀ (i j : Fin 3), LocalShell a b U (u.covariance i j))
(hV : IsSlowOn U c.base.angular)
(hG : IsSlowOn U c.base.axial)
(ho :
MeanIncrementBounds.OperatorBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU)
c.operators κ)
(hb :
MeanIncrementBounds.BaseBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) c.base)
(hm :
MeanIncrementBounds.CumulativeBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU)
u.mean)
(hangular :
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankAngular r c u n))
(haxial :
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n))
(hH : 9 / 10 ≤ H)
(i : Fin 3)
:
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U hU ε L hε hεone hL) (H + 9 / 10 - 2 * κ)
fun (n : ℕ) (x : P) => CorrectionState.debt c (VariableGaugeMean.rankStageState g r axial c u) n x i
The actual variable-gauge rank stage cancels the measured linear debt. Only local primitive/source bounds are inputs.
theorem
NavierStokes.LocalRankDefect.rankStage_defectBounds
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
{a b cL cR : ℝ}
(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)
(U : Set P)
(hU : IsOpen U)
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
{H κ : ℝ}
(hop : LocalOperators U c.operators)
(hbs : MeanIncrementBounds.SmoothTriple (positiveDomain U) c.base)
(hms : LocalTriple a b U u.mean)
(hW : ∀ (i j : Fin 3), LocalShell a b U (u.covariance i j))
(hV : IsSlowOn U c.base.angular)
(hG : IsSlowOn U c.base.axial)
(ho :
MeanIncrementBounds.OperatorBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU)
c.operators κ)
(hb :
MeanIncrementBounds.BaseBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) c.base)
(hm :
MeanIncrementBounds.CumulativeBounds (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU)
u.mean)
(hangular :
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankAngular r c u n))
(haxial :
WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) H
fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n))
(hH : 9 / 10 ≤ H)
{σ : ℝ}
(hσ : 1 + σ ≤ H + 9 / 10 - 2 * κ)
:
CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U hU ε L hε hεone hL) σ c
(VariableGaugeMean.rankStageState g r axial c u)
Support retained in the reserved moving patch #
theorem
NavierStokes.LocalRankDefect.supportedGauge_directional
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{a b : ℝ}
{ell : P → ℝ}
{U : Set P}
(hU : IsOpen U)
(hell : ContinuousOn ell U)
{f : Point P → ℝ}
(hs : VariableGaugeMean.SupportedGauge a b ell U f)
(v : Point P)
:
VariableGaugeMean.SupportedGauge a b ell U fun (p : PressureStream.Lift P) => (fderiv ℝ f p) v
Derivatives retain the moving support when its length is continuous on the open slow domain. No global continuation of the length is needed.
theorem
NavierStokes.LocalRankDefect.RankGeometry.desired_supportedGauge
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
:
VariableGaugeMean.SupportedGauge r.inner r.outer (r.length n) U
(MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n))
theorem
NavierStokes.LocalRankDefect.RankGeometry.angular_supportedGauge
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(axial : P × PressureStream.Plane)
(n : ℕ)
:
VariableGaugeMean.SupportedGauge r.inner r.outer (r.length n) U
((VariableGaugeMean.rankIncrementState g r axial c u).angular n)
theorem
NavierStokes.LocalRankDefect.RankGeometry.potential_supportedGauge
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(n : ℕ)
:
VariableGaugeMean.SupportedGauge r.inner r.outer (r.length n) U (VariableGaugeMean.rankPotential g r c u n)
The zero weighted mass prevents the primitive from spreading beyond the actual reserved rank patch.
theorem
NavierStokes.LocalRankDefect.RankGeometry.radial_supportedGauge
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
(hU : IsOpen U)
(axial : P × PressureStream.Plane)
(n : ℕ)
:
VariableGaugeMean.SupportedGauge r.inner r.outer (r.length n) U
((VariableGaugeMean.rankIncrementState g r axial c u).radial n)
theorem
NavierStokes.LocalRankDefect.RankGeometry.increment_supportedGauge
{P : Type}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
{g : VariableGaugeMean.GaugeData P}
{r : CorrectionState.RankData P}
{U : Set P}
{c : CorrectionState.Context (Point P)}
{u : CorrectionState.State (Point P)}
(hg : RankGeometry g r U c u)
[FiniteDimensional ℝ P]
{a b : ℝ}
(ha : 0 < a)
(hab : a < b)
(hU : IsOpen U)
(hleft : ∀ (n : ℕ), ∀ x ∈ U, a ≤ r.length n x * r.inner)
(hright : ∀ (n : ℕ), ∀ x ∈ U, r.length n x * r.outer ≤ b)
(axial : P × PressureStream.Plane)
(n : ℕ)
:
VariableGaugeMean.SupportedGauge r.inner r.outer (r.length n) U
((VariableGaugeMean.rankIncrementState g r axial c u).radial n) ∧ VariableGaugeMean.SupportedGauge r.inner r.outer (r.length n) U
((VariableGaugeMean.rankIncrementState g r axial c u).angular n) ∧ VariableGaugeMean.SupportedGauge r.inner r.outer (r.length n) U
((VariableGaugeMean.rankIncrementState g r axial c u).axial n)
All three actual rank components retain the same reserved moving support, including the radial derivative of the stream potential.
theorem
NavierStokes.LocalRankDefect.normalized_support_margin
{P : Type}
{a b lo hi : ℝ}
(hal : a < lo)
(hhb : hi < b)
(ell : ℕ → P → ℝ)
(U : Set P)
(f : ScalarField (Point P))
(hell : ∀ (n : ℕ), ∀ x ∈ U, 0 < ell n x)
(hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge lo hi (ell n) U (f n))
:
A fixed reserved profile interval has a uniform positive distance from both outer moving edges after division by the actual local length.