The radial residual of the actual moving pressure gauge #
The current pressure alias is subtracted literally. The remaining field is minus the normalized moving density times the measured pressure debt. Its mean class follows on the same moving strip, retaining the vanishing edge weight and all ordinary slow derivatives.
structure
NavierStokes.GaugeRadialResidualBounds.RadialMatch
(U : Set Plane)
(g : VariableGaugeMean.GaugeData Plane)
(o : MeanIncrementBounds.Operators Point)
:
Only the primitive coefficients of the actual radial derivative are matched. No residual or quantitative bound is a field of this record.
- profile (x : Point) : x.2.1 ∈ U → o.radialProfile x = RadialPullback.radialJacobian g.radial.exponent x.1
Instances For
theorem
NavierStokes.GaugeRadialResidualBounds.RadialMatch.graphOperators
(U : Set Plane)
(g : VariableGaugeMean.GaugeData Plane)
(epsilon fast : ℕ → ℝ)
(axial slowTime : Plane × Plane)
(temporal : Plane)
:
RadialMatch U g (CorrectionState.graphOperators g.radial epsilon fast axial slowTime temporal)
theorem
NavierStokes.GaugeRadialResidualBounds.RadialMatch.nativeOperators
(U : Set Plane)
(g : VariableGaugeMean.GaugeData Plane)
(epsilon fast : ℕ → ℝ)
(axial slowTime temporal : Plane)
:
RadialMatch U g (StateMomentBalances.nativeOperators g.radial epsilon fast axial slowTime temporal)
theorem
NavierStokes.GaugeRadialResidualBounds.RadialMatch.dr
{U : Set Plane}
{g : VariableGaugeMean.GaugeData Plane}
{o : MeanIncrementBounds.Operators Point}
(H : RadialMatch U g o)
(f : Scalar)
(n : ℕ)
{x : Point}
(hx : x.2.1 ∈ U)
:
o.dr f n x = PressureStream.graphDr (PressureStream.physicalSpeed g.radial.exponent (g.radial.frequency n))
(0, g.radial.radialDirection) (f n) x
The primitive matches give the genuine derivative identity for every field, without requiring differentiability to identify the two operators.
noncomputable def
NavierStokes.GaugeRadialResidualBounds.radialMinusAlias
(g : VariableGaugeMean.GaugeData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
The literal radial component after removing the current pressure alias.
Equations
- NavierStokes.GaugeRadialResidualBounds.radialMinusAlias g c u n x = u.radialResidual c n x - NavierStokes.VariableGaugeMean.pressureAliasState g c u n (x, 0) 0
Instances For
theorem
NavierStokes.GaugeRadialResidualBounds.radialMinusAlias_angle
(g : VariableGaugeMean.GaugeData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(n : ℕ)
(x : Point)
(theta : ℝ)
:
u.radialResidual c n x - VariableGaugeMean.pressureAliasState g c u n (x, theta) 0 = radialMinusAlias g c u n x
theorem
NavierStokes.GaugeRadialResidualBounds.pressureDefect_eq_mass
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(n : ℕ)
(s : Plane)
:
The pressure defect is the actual zeroth radial moment of the radial source, with the same auxiliary-torus average used by the gauge.
theorem
NavierStokes.GaugeRadialResidualBounds.primitiveData_reconstructState
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
(g : VariableGaugeMean.GaugeData Plane)
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U a b c u)
:
MeanStateRegularity.PrimitiveData U a b c (VariableGaugeMean.reconstructState g c u)
Pressure reconstruction preserves every primitive input field: this record deliberately contains no output regularity assertion for pressure.
theorem
NavierStokes.GaugeRadialResidualBounds.radialMinusAlias_identity
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hr : RadialMatch U.carrier g c.operators)
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
(n : ℕ)
{x : Point}
(hx : x.2.1 ∈ U.carrier)
:
radialMinusAlias g c u n x = -VariableGaugeMean.density g.radial.inner g.radial.outer ⋯ (g.length n) x * CorrectionState.pressureDefect c u n x.2.1
Primitive field regularity supplies the source regularity and support. Only the pressure reconstruction equality is required of the incoming state.
theorem
NavierStokes.GaugeRadialResidualBounds.reconstructed_identity
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hr : RadialMatch U.carrier g c.operators)
(n : ℕ)
{x : Point}
(hx : x.2.1 ∈ U.carrier)
:
radialMinusAlias g c (VariableGaugeMean.reconstructState g c u) n x = -VariableGaugeMean.density g.radial.inner g.radial.outer ⋯ (g.length n) x * CorrectionState.pressureDefect c u n x.2.1
Applying the actual constructor discharges pressure reconstruction; the same incoming primitive data and pressure debt are used.
theorem
NavierStokes.GaugeRadialResidualBounds.density_times_debt_class
{coord cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(ha : 0 < g.radial.inner)
(hcL : 0 < cL)
(hcR : 0 < cR)
(epsilon slow : ℕ → ℝ)
(hepsilon : ∀ (n : ℕ), 0 < epsilon n)
(hepsilon_one : ∀ (n : ℕ), epsilon n ≤ 1)
(hslow : ∀ (n : ℕ), 1 ≤ slow n)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
{alpha : ℝ}
{debt : ℕ → Plane → ℝ}
(hdebt :
WeightedClasses.UnweightedClass
(PhysicalMeanDomain.localSlowStripData U.carrier ⋯ epsilon slow hepsilon hepsilon_one hslow) alpha debt)
:
WeightedClasses.MeanClass
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR epsilon slow hepsilon
hepsilon_one hslow)
alpha fun (n : ℕ) (x : LocalSignedRequest.Point) =>
-VariableGaugeMean.density g.radial.inner g.radial.outer ⋯ (g.length n) x * debt n x.2.1
The measured slow debt lifts without loss and multiplies the actual normalized moving density. The density contributes the genuine edge weight.
theorem
NavierStokes.GaugeRadialResidualBounds.radialMinusAlias_class
{coord cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hcL : 0 < cL)
(hcR : 0 < cR)
(epsilon slow : ℕ → ℝ)
(hepsilon : ∀ (n : ℕ), 0 < epsilon n)
(hepsilon_one : ∀ (n : ℕ), epsilon n ≤ 1)
(hslow : ∀ (n : ℕ), 1 ≤ slow n)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hr : RadialMatch U.carrier g c.operators)
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
{alpha : ℝ}
(hdebt :
WeightedClasses.UnweightedClass
(PhysicalMeanDomain.localSlowStripData U.carrier ⋯ epsilon slow hepsilon hepsilon_one hslow) alpha
(CorrectionState.pressureDefect c u))
:
WeightedClasses.MeanClass
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR epsilon slow hepsilon
hepsilon_one hslow)
alpha (radialMinusAlias g c u)
The literal radial residual minus its current pressure alias has exactly the measured debt's order on the same moving strip. No source class is assumed.
theorem
NavierStokes.GaugeRadialResidualBounds.reconstructed_class
{coord cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hcL : 0 < cL)
(hcR : 0 < cR)
(epsilon slow : ℕ → ℝ)
(hepsilon : ∀ (n : ℕ), 0 < epsilon n)
(hepsilon_one : ∀ (n : ℕ), epsilon n ≤ 1)
(hslow : ∀ (n : ℕ), 1 ≤ slow n)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(H : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(hr : RadialMatch U.carrier g c.operators)
{alpha : ℝ}
(hdebt :
WeightedClasses.UnweightedClass
(PhysicalMeanDomain.localSlowStripData U.carrier ⋯ epsilon slow hepsilon hepsilon_one hslow) alpha
(CorrectionState.pressureDefect c u))
:
WeightedClasses.MeanClass
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR epsilon slow hepsilon
hepsilon_one hslow)
alpha (radialMinusAlias g c (VariableGaugeMean.reconstructState g c u))
The actual reconstructed state's radial class is derived without an input assertion that its pressure already equals the gauge formula.
theorem
NavierStokes.GaugeRadialResidualBounds.similarity_identity
{h a b : ℝ}
(U : LocalSignedRequest.SlowRegion (2 * h))
(ha : 0 < a)
(hab : a < b)
(Mbase : ℝ)
(index : ℕ → ℕ)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(H : MeanStateRegularity.PrimitiveData U a b c u)
(hr :
RadialMatch U.carrier (VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index)
c.operators)
(hfixed :
(VariableGaugeMean.reconstructState
(VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u).pressure = u.pressure)
(n : ℕ)
{x : Point}
(hx : x.2.1 ∈ U.carrier)
:
u.radialResidual c n x - VariableGaugeMean.pressureAliasState
(VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u n (x, 0) 0 = -VariableGaugeMean.density a b hab (VariableGaugeMean.qLength (2 * h)) x * CorrectionState.pressureDefect c u n x.2.1
The normalized bump and sign for the actual similarity gauge.
theorem
NavierStokes.GaugeRadialResidualBounds.similarity_class
{h a b cL cR sigma : ℝ}
(U : LocalSignedRequest.SlowRegion (2 * h))
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
(Mbase : ℝ)
(index : ℕ → ℕ)
(epsilon slow : ℕ → ℝ)
(hepsilon : ∀ (n : ℕ), 0 < epsilon n)
(hepsilon_one : ∀ (n : ℕ), epsilon n ≤ 1)
(hslow : ∀ (n : ℕ), 1 ≤ slow n)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(H : MeanStateRegularity.PrimitiveData U a b c u)
(hr :
RadialMatch U.carrier (VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index)
c.operators)
(hfixed :
(VariableGaugeMean.reconstructState
(VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u).pressure = u.pressure)
(hdebt :
WeightedClasses.UnweightedClass
(PhysicalMeanDomain.localSlowStripData U.carrier ⋯ epsilon slow hepsilon hepsilon_one hslow) (1 + sigma)
(CorrectionState.pressureDefect c u))
:
WeightedClasses.MeanClass
(LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR epsilon slow hepsilon hepsilon_one hslow) (1 + sigma)
fun (n : ℕ) (x : LocalSignedRequest.Point) =>
u.radialResidual c n x - VariableGaugeMean.pressureAliasState
(VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u n (x, 0) 0
The iteration's radial component: an S_(1+sigma) pressure debt gives M_(1+sigma) for the current alias-subtracted radial residual.
theorem
NavierStokes.GaugeRadialResidualBounds.similarity_native_class
{h a b cL cR sigma : ℝ}
(U : LocalSignedRequest.SlowRegion (2 * h))
(ha : 0 < a)
(hab : a < b)
(hcL : 0 < cL)
(hcR : 0 < cR)
(Mbase : ℝ)
(index : ℕ → ℕ)
(epsilon slow : ℕ → ℝ)
(hepsilon : ∀ (n : ℕ), 0 < epsilon n)
(hepsilon_one : ∀ (n : ℕ), epsilon n ≤ 1)
(hslow : ∀ (n : ℕ), 1 ≤ slow n)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(H : MeanStateRegularity.PrimitiveData U a b c u)
(fast : ℕ → ℝ)
(axial slowTime temporal : Plane)
(ho :
c.operators = StateMomentBalances.nativeOperators
(VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index).radial epsilon fast axial
slowTime temporal)
(hfixed :
(VariableGaugeMean.reconstructState
(VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u).pressure = u.pressure)
(hdebt :
WeightedClasses.UnweightedClass
(PhysicalMeanDomain.localSlowStripData U.carrier ⋯ epsilon slow hepsilon hepsilon_one hslow) (1 + sigma)
(CorrectionState.pressureDefect c u))
:
WeightedClasses.MeanClass
(LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR epsilon slow hepsilon hepsilon_one hslow) (1 + sigma)
fun (n : ℕ) (x : LocalSignedRequest.Point) =>
u.radialResidual c n x - VariableGaugeMean.pressureAliasState
(VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b Mbase hab index) c u n (x, 0) 0
With the actual native operators, every radial matching field is proved from the constructor. The only operator premise is the literal input binding.