Residual estimates from the actual correction-cycle invariant #
The primary family, common chart, weighted strip and carrier sets below are
the actual selected objects. Finite harmonic bounds are read from sourceBand.
Joint flatness of the actual excluded slow-base error #
One fixed schedule controls its entire compact similarity box. Beyond that box the actual residual and virtual stress force both vanish, so the error vanishes in every jet. The resulting estimates impose no upper bound on the similarity radius of the approach to the origin.
The field estimated here is FinalSlowBase.error, which is the actual
Navier--Stokes residual minus its virtual stress force.
theorem
NavierStokes.GlobalBaseError.cartesian_q_pos
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{z : ProblemStatement.SpaceTime}
(ht : z.1 < 1)
:
theorem
NavierStokes.GlobalBaseError.cartesian_X_nonneg
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{z : ProblemStatement.SpaceTime}
(ht : z.1 < 1)
:
theorem
NavierStokes.GlobalBaseError.cartesian_q_tendsto_zero
{l : Filter ProblemStatement.SpaceTime}
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hl : Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => z) l (nhds (1, 0)))
(ht : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z.1 < 1)
:
Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) l (nhds 0)
The actual implicit scale tends to zero on a joint approach, without
any bound on X = radialEnergy / q.
theorem
NavierStokes.GlobalBaseError.exteriorRadius_le_box
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
{upper : ℝ}
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
:
The original schedule box contains both the supplied upper radius and the end of the active stress annulus.
theorem
NavierStokes.GlobalBaseError.error_zero_outside_box
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
{z : ProblemStatement.SpaceTime}
(ht : z.1 < 1)
(hX : FinalSlowBase.boxRadius W upper < (SlowBorelBase.cartesianChart F.data.h z).2.1)
:
theorem
NavierStokes.GlobalBaseError.error_germ_zero_outside_box
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
{z : ProblemStatement.SpaceTime}
(ht : z.1 < 1)
(hX : FinalSlowBase.boxRadius W upper < (SlowBorelBase.cartesianChart F.data.h z).2.1)
:
The exterior equalities hold on an open neighborhood, so they control all actual derivatives of the error, not only its value.
theorem
NavierStokes.GlobalBaseError.error_jets_zero_outside_box
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B m : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
{z : ProblemStatement.SpaceTime}
(ht : z.1 < 1)
(hX : FinalSlowBase.boxRadius W upper < (SlowBorelBase.cartesianChart F.data.h z).2.1)
:
theorem
NavierStokes.GlobalBaseError.error_jetRate
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
{l : Filter ProblemStatement.SpaceTime}
{K : Set ProblemStatement.SpaceTime}
(hK : IsCompact K)
(hcarrier : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ K)
(ht : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z.1 < 1)
(hq : Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) l (nhds 0))
(m : ℕ)
(r : ℝ)
(hr : 0 ≤ r)
:
DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1)
(FinalSlowBase.error H v upper B) m r
An arbitrary physical approach with compact carrier and q → 0 is
allowed. Its similarity radius need not be bounded. The scale sequence in
FinalSlowBase.error H v upper B is unchanged between the two regions.
theorem
NavierStokes.GlobalBaseError.error_allJetsFlat
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
{l : Filter ProblemStatement.SpaceTime}
{K : Set ProblemStatement.SpaceTime}
(hK : IsCompact K)
(hcarrier : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ K)
(ht : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z.1 < 1)
(hq : Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) l (nhds 0))
:
ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1)
(FinalSlowBase.error H v upper B)
The joint past filter at the physical origin #
Origin past, given by 𝓝[SpacetimeEndpoint.openPast 1] ((1 : ℝ), (0 : Space)).
Equations
Instances For
theorem
NavierStokes.GlobalBaseError.originPast_before :
∀ᶠ (z : ProblemStatement.SpaceTime) in originPast, z.1 < 1
theorem
NavierStokes.GlobalBaseError.originPast_tendsto :
Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => z) originPast (nhds (1, 0))
theorem
NavierStokes.GlobalBaseError.originPast_in_compact :
∀ᶠ (z : ℝ × ProblemStatement.Space) in originPast, z ∈ Metric.closedBall (1, 0) 1
theorem
NavierStokes.GlobalBaseError.originPast_q_tendsto_zero
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
:
Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) originPast (nhds 0)
theorem
NavierStokes.GlobalBaseError.error_joint_jetRate
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
(m : ℕ)
(r : ℝ)
(hr : 0 ≤ r)
:
DiagonalResidual.JetRate originPast
(fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1)
(FinalSlowBase.error H v upper B) m r
theorem
NavierStokes.GlobalBaseError.error_joint_allJetsFlat
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
:
ResidualStability.AllJetsFlat originPast
(fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1)
(FinalSlowBase.error H v upper B)
theorem
NavierStokes.GlobalBaseError.error_vanishingJointJets
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(upper : ℝ)
(B : ℕ)
(hupper : BaseExterior.nominalExteriorRadius W ≤ upper)
:
JointResidualLimits.VanishingJointJets (FinalSlowBase.error H v upper B)
Full joint vanishing of all actual error jets at (1,0) from the past,
with no bounded-similarity-radius premise.
One actual profile and one fixed enlarged schedule #
The enlargement depends only on the originally selected profile and
the supplied constant, never on the physical point, derivative order, or q.
Equations
Instances For
Actual error, given by FinalSlowBase.error FinalSlowBase.actualProfile.certificate FinalSlowBase.actualProfile.modulation (actualUpper upper) B.
Equations
Instances For
theorem
NavierStokes.GlobalBaseError.actual_error_joint_jetRate
(upper : ℝ)
(B m : ℕ)
(r : ℝ)
(hr : 0 ≤ r)
:
DiagonalResidual.JetRate originPast
(fun (z : ProblemStatement.SpaceTime) =>
(SlowBorelBase.cartesianChart FinalSlowBase.actualProfile.outgoing.data.h z).1)
(actualError upper B) m r
theorem
NavierStokes.GlobalBaseError.actual_error_joint_allJetsFlat
(upper : ℝ)
(B : ℕ)
:
ResidualStability.AllJetsFlat originPast
(fun (z : ProblemStatement.SpaceTime) =>
(SlowBorelBase.cartesianChart FinalSlowBase.actualProfile.outgoing.data.h z).1)
(actualError upper B)
noncomputable def
NavierStokes.ActualCycleResidualBounds.labelCarrier
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
:
Label carrier, given by ActualInitialExcluded.labelCarrier (l.2, l.1) n.
Equations
Instances For
theorem
NavierStokes.ActualCycleResidualBounds.labelCarrier_closed
{B N0 : ℕ}
(l : Index B N0)
(n : ℕ)
:
IsClosed (labelCarrier l n)
@[reducible, inline]
abbrev
NavierStokes.ActualCycleResidualBounds.Invariant
{B N0 : ℕ}
(σ : ℝ)
(x : CorrectionStep.CycleState (Index B N0))
:
Invariant type used in actual cycle residual bounds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ActualCycleResidualBounds.source
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Index B N0))
(l : Index B N0)
:
Source, constructed using HarmonicResidual.residualBlock.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_support
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
(n : ℕ)
(i : Fin 3)
:
((source x l).velocity n i).support ⊆ modes x.coefficients.residualBand
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_carrier
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_fullPhase
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
(j : ℤ)
(n : ℕ)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_zero_germ
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
(j : ℤ)
(n : ℕ)
{z : Point}
(hz : z ∈ ActualInitialization.geometry.domain)
(hout : z ∉ labelCarrier l n)
:
theorem
NavierStokes.ActualCycleResidualBounds.actual_flatGeometry :
∃ (cL : ℝ) (cR : ℝ) (L : ℝ) (ρ : Point → ℝ),
PhysicalClassBounds.FlatGeometry ActualInitialization.geometry.strip cL cR L ρ
theorem
NavierStokes.ActualCycleResidualBounds.actual_wave_weight
{B N0 : ℕ}
:
∃ (c : ℝ),
0 < c ∧ ∀ (l : Index B N0) (n : ℕ),
∀ z ∈ ActualInitialization.geometry.strip.domain,
√(ActualInitialization.geometry.strip.zeta z) * ActualInitialization.envelope l n z ≤ ActualInitialization.geometry.strip.zeta z ^ c
theorem
NavierStokes.ActualCycleResidualBounds.mean_source
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{α : ℝ}
{f : ℕ → Point → E}
(hf : WeightedClasses.MeanClass ActualInitialization.geometry.strip α f)
:
LocalPhysicalCopyBounds.LocalSourceBounds ActualInitialization.geometry.strip CorrectionInitialization.ActualPrimary.h α
(fun (x : Unit) (x_1 : ℕ) (z : SignedMeanGain.Point) => ActualInitialization.geometry.strip.zeta z) fun (x : Unit) =>
f
theorem
NavierStokes.ActualCycleResidualBounds.sqrt_source
{ι E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{α : ℝ}
{f : ι → ℕ → Point → E}
(hf :
LabelSumBounds.UniformClass ActualInitialization.geometry.strip
(fun (x : ι) (x_1 : ℕ) (z : SignedMeanGain.Point) => √(ActualInitialization.geometry.strip.zeta z)) α f)
:
LocalPhysicalCopyBounds.LocalSourceBounds ActualInitialization.geometry.strip CorrectionInitialization.ActualPrimary.h α
(fun (x : ι) (x_1 : ℕ) (z : SignedMeanGain.Point) => √(ActualInitialization.geometry.strip.zeta z)) f
theorem
NavierStokes.ActualCycleResidualBounds.native_on_strip
{ι E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{α : ℝ}
{w : ι → ℕ → Point → ℝ}
{f : ι → ℕ → Point → E}
(hf :
LocalPhysicalCopyBounds.LocalSourceBounds ActualInitialization.geometry.strip CorrectionInitialization.ActualPrimary.h
α w f)
:
PhysicalResidualJetBounds.NativeBounds 4 ActualInitialization.geometry.strip.domain
(CorrectionInitialization.ActualPrimary.h * α) (fun (x : ℕ) => 0) f
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_localBounds
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(i : Fin 3)
(j : ℤ)
(hj : j ≠ 0)
:
LocalPhysicalCopyBounds.LocalSourceBounds ActualInitialization.geometry.strip CorrectionInitialization.ActualPrimary.h
(1 / 2 + σ)
(fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : SignedMeanGain.Point) =>
√(ActualInitialization.geometry.strip.zeta z) * ActualInitialization.envelope l n z)
fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : SignedMeanGain.Point) => ((source x l).velocity n i).coeff j z
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(i : Fin 3)
(j : ℤ)
:
PhysicalResidualJetBounds.NativeBounds 4 ActualInitialization.geometry.strip.domain
(CorrectionInitialization.ActualPrimary.h * (1 / 2 + σ)) (fun (x : ℕ) => 0)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) => ((source x l).velocity n i).coeff j z
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(α : ℝ)
(i : Fin 3)
(j : ℤ)
:
PhysicalResidualJetBounds.NativeBounds 4 ActualInitialization.geometry.strip.domain
(CorrectionInitialization.ActualPrimary.h * α) (fun (x : ℕ) => 0)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) => (x.coefficients.gaussian l n i).coeff j z
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.axis_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(α : ℝ)
:
PhysicalResidualJetBounds.NativeBounds 4 ActualInitialization.geometry.strip.domain
(CorrectionInitialization.ActualPrimary.h * α) (fun (x : ℕ) => 0) fun (x_1 : Unit) => x.axisymmetricAlias
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.current_pressureAlias_class
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(α : ℝ)
:
The current pressure alias has every power, by the actual compact primitive and gauge estimates, independently of the accumulated alias.
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.alias_eq_lift
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
:
x.state.errors.aliasError = fun (n : ℕ) (z : CorrectionStep.CyclePoint × ℝ) => x.axisymmetricAlias n z.1
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.meanGood_eq_reduced_sub
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(n : ℕ)
{z : Point}
(hz : z ∈ ActualInitialization.geometry.strip.domain)
(i : Fin 3)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.radial_mean_class
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
:
WeightedClasses.MeanClass ActualInitialization.geometry.strip (1 + σ) fun (n : ℕ) (z : SignedMeanGain.Point) =>
x.state.meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n z 0
The missing radial component is derived from the measured pressure debt, the literal reconstructed pressure and the current compact alias.
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.mean_component_class
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(i : Fin 3)
:
WeightedClasses.MeanClass ActualInitialization.geometry.strip (1 + σ) fun (n : ℕ) (z : SignedMeanGain.Point) =>
x.state.meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n z i
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.mean_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
:
PhysicalResidualJetBounds.NativeBounds 4 ActualInitialization.geometry.strip.domain
(CorrectionInitialization.ActualPrimary.h * (1 + σ)) (fun (x : ℕ) => 0) fun (x_1 : Unit) =>
x.state.meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B)
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.extraction_regular
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(n : ℕ)
(hdisj :
∀ l ∈ x.coefficients.labels n,
∀ k ∈ x.coefficients.labels n,
l ≠ k →
Disjoint
(HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain ∩ tsupport ((x.coefficients.blocks l).oscillation n))
(HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain ∩ tsupport ((x.coefficients.blocks k).oscillation n)))
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.fullResidual_decomposition
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
{n : ℕ}
(hreg :
LocalResidualGrouping.ExtractionRegular ActualInitialization.geometry.strip.domain
(CorrectionInitialization.ActualPrimary.commonContext B) x.state x.coefficients.labels x.coefficients.blocks
x.coefficients.gaussian x.coefficients.aliasCoefficients n)
{z : Cylinder}
(hz : z ∈ HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(i : Fin 3)
:
LiftedMeanResidual.fullResidual (CorrectionInitialization.ActualPrimary.commonContext B) x.state n z i = ∑ l ∈ x.coefficients.labels n, (source x l).oscillation n z i + x.state.meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n z.1 i + x.state.errors.total n z i
The independent accumulated axisymmetric alias is retained in the grouping and cancels only through the proved angular mean equation.
theorem
NavierStokes.ActualCycleResidualBounds.native_restrict
{D E ι : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{N M : ℕ}
{U V : Set D}
{gain : ℝ}
{loss : ℕ → ℝ}
{f : ι → ℕ → D → E}
(hf : PhysicalResidualJetBounds.NativeBounds N U gain loss f)
(hNM : N ≤ M)
(hVU : V ⊆ U)
:
PhysicalResidualJetBounds.NativeBounds M V gain loss f
theorem
NavierStokes.ActualCycleResidualBounds.native_lift
{E ι : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{N : ℕ}
{U : Set Point}
{gain : ℝ}
{loss : ℕ → ℝ}
{f : ι → ℕ → Point → E}
(hU : IsOpen U)
(hf : PhysicalResidualJetBounds.NativeBounds N U gain loss f)
:
PhysicalResidualJetBounds.NativeBounds N (HarmonicResidual.liftDomain U) gain loss fun (l : ι) (n : ℕ) (z : Cylinder) =>
f l n z.1
theorem
NavierStokes.ActualCycleResidualBounds.normalizedBase_native
(B : ℕ)
(α : ℝ)
:
PhysicalResidualJetBounds.NativeBounds 4
(BaseContextAssembly.slowCarrier CorrectionInitialization.ActualPrimary.nominal
CorrectionInitialization.ActualPrimary.standardRegion)
(CorrectionInitialization.ActualPrimary.h * α) (fun (x : ℕ) => 0) fun (x : Unit) =>
ActualInitialExcluded.normalizedBase CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B
theorem
NavierStokes.ActualCycleResidualBounds.baseError_native
(B : ℕ)
(α : ℝ)
:
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(CorrectionInitialization.ActualPrimary.h * α) (fun (x : ℕ) => 0) fun (x : Unit) => ActualInitialization.baseError B
The fixed base error uses its actual all-power physical estimate. No flat edge weight is incorrectly assigned to this term.
theorem
NavierStokes.ActualCycleResidualBounds.graphResidual_smooth
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : Set E}
(hU : IsOpen U)
(ε : ℝ)
{R : E → ℝ}
{Vr Vθ Vz Vt : E → E}
{a : E → Fin 3 → ℝ}
{p : E → ℝ}
(hR : ContDiffOn ℝ (↑⊤) R U)
(hRne : ∀ z ∈ U, R z ≠ 0)
(hr : ContDiffOn ℝ (↑⊤) Vr U)
(hθ : ContDiffOn ℝ (↑⊤) Vθ U)
(hz : ContDiffOn ℝ (↑⊤) Vz U)
(ht : ContDiffOn ℝ (↑⊤) Vt U)
(ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (z : E) => a z i) U)
(hp : ContDiffOn ℝ (↑⊤) p U)
:
ContDiffOn ℝ (↑⊤) (PhysicalResidualBridge.graphResidual ε R Vr Vθ Vz Vt a p) U
Smoothness of the actual full graph operator follows from its primitive coefficients and their actual directional derivatives.
theorem
NavierStokes.ActualCycleResidualBounds.realization_native_smooth
{h : ℝ}
{N : ℕ}
{gap : ℕ → ℕ}
{U : Set Cylinder}
{c : CorrectionState.Context Point}
{s : CorrectionState.State Point}
{p₀ : ℕ → Cylinder → ℝ}
{u : ProblemStatement.VelocityField}
{P : ProblemStatement.PressureField}
(r : PhysicalResidualJetBounds.StateRealization h N gap U c s p₀ u P)
{n : ℕ}
(hn : N ≤ n)
:
ContDiffOn ℝ (↑⊤) (LiftedMeanResidual.fullResidual c s n) U
The local primitive realization also supplies smoothness of the full native residual across the radial edges. It is not an output-jet premise.
The fixed exterior base and the full physical endpoint #
theorem
NavierStokes.ActualCycleResidualBounds.base_residual_germ
(B : ℕ)
{w : ProblemStatement.SpaceTime}
(hw : w ∈ PhysicalWaveSum.preterminal)
(hout : w ∉ active)
:
PhysicalResidualJetBounds.residual
(FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B)
(FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B) =ᶠ[nhds w] FinalSlowBase.error CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B
theorem
NavierStokes.ActualCycleResidualBounds.base_exterior_jetRate
(B m : ℕ)
(r : ℝ)
:
DiagonalResidual.JetRate (GlobalBaseError.originPast ⊓ Filter.principal activeᶜ)
(PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h)
(PhysicalResidualJetBounds.residual
(FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B)
(FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B))
m r
Actual carriers, phases, and bounded label sums #
noncomputable def
NavierStokes.ActualCycleResidualBounds.gaussianModes
{B N0 : ℕ}
(x : CorrectionStep.CycleState (Index B N0))
(l : Index B N0)
:
Gaussian modes, bundling velocity, pressure, frequency, phase and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleResidualBounds.coefficient_tsupport_carrier
{B N0 : ℕ}
{E : Type}
[NormedAddCommGroup E]
{l : Index B N0}
{n : ℕ}
{a : Point → E}
(ha : ∀ z ∈ ActualInitialization.geometry.domain, z ∉ labelCarrier l n → a z = 0)
{z : Cylinder}
(hz : z ∈ HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(hs : z ∈ tsupport fun (y : Cylinder) => a y.1)
:
theorem
NavierStokes.ActualCycleResidualBounds.oscillation_eq_zero_of_coefficients
(b : CorrectionState.HarmonicBlock Point)
(n : ℕ)
(z : Cylinder)
(hb : ∀ (i : Fin 3) (j : ℤ), (b.velocity n i).coeff j z.1 = 0)
:
theorem
NavierStokes.ActualCycleResidualBounds.oscillation_tsupport_carrier
{B N0 : ℕ}
{l : Index B N0}
{n : ℕ}
{b : CorrectionState.HarmonicBlock Point}
(hb :
∀ z ∈ ActualInitialization.geometry.domain,
z ∉ labelCarrier l n → ∀ (i : Fin 3) (j : ℤ), (b.velocity n i).coeff j z = 0)
{z : Cylinder}
(hz : z ∈ HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(hs : z ∈ tsupport (b.oscillation n))
:
theorem
NavierStokes.ActualCycleResidualBounds.fullPhase_eq_weighted
{B N0 : ℕ}
(b : Index B N0 → CorrectionState.HarmonicBlock Point)
(hc : ∀ (l : Index B N0), CorrectionStep.SameCarrier (b l) (ActualInitialization.primaryBlock l))
(l : Index B N0)
(j : ℤ)
(n : ℕ)
:
PhysicalResidualJetBounds.fullPhase (b l) j n = fun (z : CorrectionInitialization.ActualPrimary.FullPoint) =>
↑j * ActualPhaseJetBounds.weightedPhase (l.2, l.1) n z
theorem
NavierStokes.ActualCycleResidualBounds.supportedPhaseBounds
{B N0 : ℕ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(b : Index B N0 → CorrectionState.HarmonicBlock Point)
(hc : ∀ (l : Index B N0), CorrectionStep.SameCarrier (b l) (ActualInitialization.primaryBlock l))
(a : Index B N0 → ℕ → Point → ℂ)
(ha : ∀ (l : Index B N0) (n : ℕ), ∀ z ∈ ActualInitialization.geometry.domain, z ∉ labelCarrier l n → a l n z = 0)
(j : ℤ)
:
PhysicalResidualJetBounds.SupportedPhaseBounds 4
(HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(2 * CorrectionInitialization.ActualPrimary.h)
(fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point × ℝ) => a l n z.1) fun (l : Index B N0) =>
PhysicalResidualJetBounds.fullPhase (b l) j
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_coeff_zero_off
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
(n : ℕ)
(z : Point)
(hz : z ∈ ActualInitialization.geometry.domain)
(hn : z ∉ labelCarrier l n)
(i : Fin 3)
(j : ℤ)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.wave_coeff_zero_off
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
(n : ℕ)
(z : Point)
(hz : z ∈ ActualInitialization.geometry.domain)
(hn : z ∉ labelCarrier l n)
(i : Fin 3)
(j : ℤ)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_coeff_zero_off
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
(n : ℕ)
(z : Point)
(hz : z ∈ ActualInitialization.geometry.domain)
(hn : z ∉ labelCarrier l n)
(i : Fin 3)
(j : ℤ)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.actual_disjoint
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(n : ℕ)
{l k : Index B N0}
(hlk : l ≠ k)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.actual_extraction_regular
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(n : ℕ)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_phase
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(i : Fin 3)
(j : ℤ)
:
PhysicalResidualJetBounds.SupportedPhaseBounds 4
(HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(2 * CorrectionInitialization.ActualPrimary.h)
(fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point × ℝ) => ((source x l).velocity n i).coeff j z.1)
fun (l : Index B N0) => PhysicalResidualJetBounds.fullPhase (source x l) j
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_oscillation_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
:
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(CorrectionInitialization.ActualPrimary.h * (1 / 2 + σ))
(fun (m : ℕ) => 2 * CorrectionInitialization.ActualPrimary.h * ↑m) fun (l : Index B N0) => (source x l).oscillation
theorem
NavierStokes.ActualCycleResidualBounds.block_window_sum
{B N0 : ℕ}
{gain : ℝ}
{loss : ℕ → ℝ}
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(labels : ℕ → Finset (Index B N0))
(b : Index B N0 → CorrectionState.HarmonicBlock Point)
(hzero :
∀ (l : Index B N0) (n : ℕ),
∀ z ∈ ActualInitialization.geometry.domain,
z ∉ labelCarrier l n → ∀ (i : Fin 3) (j : ℤ), ((b l).velocity n i).coeff j z = 0)
(hb :
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain) gain
loss fun (l : Index B N0) => (b l).oscillation)
:
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain) gain
loss fun (x : Unit) (n : ℕ) (z : SignedMeanGain.Point × ℝ) => ∑ l ∈ labels n, (b l).oscillation n z
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_modes_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(α : ℝ)
(i : Fin 3)
(j : ℤ)
:
PhysicalResidualJetBounds.NativeBounds 4 ActualInitialization.geometry.strip.domain
(CorrectionInitialization.ActualPrimary.h * α) (fun (x : ℕ) => 0)
fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point) => ((gaussianModes x l).velocity n i).coeff j z
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_carrier
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(l : Index B N0)
:
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_phase
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(i : Fin 3)
(j : ℤ)
:
PhysicalResidualJetBounds.SupportedPhaseBounds 4
(HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(2 * CorrectionInitialization.ActualPrimary.h)
(fun (l : Index B N0) (n : ℕ) (z : SignedMeanGain.Point × ℝ) => ((gaussianModes x l).velocity n i).coeff j z.1)
fun (l : Index B N0) => PhysicalResidualJetBounds.fullPhase (gaussianModes x l) j
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_oscillation_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(α : ℝ)
:
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(CorrectionInitialization.ActualPrimary.h * α) (fun (m : ℕ) => 2 * CorrectionInitialization.ActualPrimary.h * ↑m)
fun (l : Index B N0) => (gaussianModes x l).oscillation
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_modes_sum
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(n : ℕ)
(z : Cylinder)
:
Removing each zero Fourier mode preserves the total Gaussian field: the sum of those modes is its actual angular mean, which is zero.
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.source_sum_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
:
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(CorrectionInitialization.ActualPrimary.h * (1 / 2 + σ))
(fun (m : ℕ) => 2 * CorrectionInitialization.ActualPrimary.h * ↑m)
fun (x_1 : Unit) (n : ℕ) (z : SignedMeanGain.Point × ℝ) => ∑ l ∈ x.coefficients.labels n, (source x l).oscillation n z
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.gaussian_field_native
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(α : ℝ)
:
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(CorrectionInitialization.ActualPrimary.h * α) (fun (m : ℕ) => 2 * CorrectionInitialization.ActualPrimary.h * ↑m)
fun (x_1 : Unit) => x.state.errors.gaussian
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.native_residual
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
(hN : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hbase : x.state.errors.base = ActualInitialization.baseError B)
:
PhysicalResidualJetBounds.NativeBounds 4 (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)
(CorrectionInitialization.ActualPrimary.h * (1 / 2 + σ))
(fun (m : ℕ) => 2 * CorrectionInitialization.ActualPrimary.h * ↑m) fun (x_1 : Unit) =>
LiftedMeanResidual.fullResidual (CorrectionInitialization.ActualPrimary.commonContext B) x.state
Every term of the literal state residual has the required native gain. The phase loss is fixed once, independently of the cycle index.
theorem
NavierStokes.ActualCycleResidualBounds.iterate_base_error
{ι : Type}
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(J : ℕ)
:
The four operations retain the same fixed base error at every stage.
theorem
NavierStokes.ActualCycleResidualBounds.actual_iterate_base_error
{B N0 : ℕ}
(p : ℕ → CorrectionStep.CycleParameters (Index B N0))
(J : ℕ)
:
Restriction through the selected dyadic band, including radial edges #
structure
NavierStokes.ActualCycleResidualBounds.SelectedGeometry
(a b h : ℝ)
(N Δ : ℕ)
(gap : ℕ → ℕ)
(U V : Set Cylinder)
(S : Set ProblemStatement.SpaceTime)
:
These are geometric statements about the single band actually selected by the dyadic argument. The upper comparison is strict.
- annulus (n : ℕ) : N ≤ n → ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n → ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ h w → w ∈ S → (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b
- in_domain (n : ℕ) : N ≤ n → ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n → ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ h w → w ∈ S → ∀ (j : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j → PhysicalResidualJetBounds.polarGraph a h j n (gap n) w ∈ U
- in_closure (n : ℕ) : N ≤ n → ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n → ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ h w → w ∈ S → ∀ (j : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j → PhysicalResidualJetBounds.polarGraph a h j n (gap n) w ∈ closure V
Instances For
theorem
NavierStokes.ActualCycleResidualBounds.selected_residual_jet_bound
{a b h gain β : ℝ}
{N Δ : ℕ}
{gap : ℕ → ℕ}
{U V : Set Cylinder}
{S : Set ProblemStatement.SpaceTime}
{c : CorrectionState.Context Point}
{s : CorrectionState.State Point}
{p₀ : ℕ → Cylinder → ℝ}
{u : ProblemStatement.VelocityField}
{P : ProblemStatement.PressureField}
(r : PhysicalResidualJetBounds.StateRealization h N gap U c s p₀ u P)
(g : SelectedGeometry a b h N Δ gap U V S)
(hh : 0 < h)
(hh1 : h < 1 / 2)
(ha : 0 < a)
(hN : 4 ≤ N)
(hf :
PhysicalResidualJetBounds.NativeBounds N V gain (fun (m : ℕ) => β * ↑m) fun (x : Unit) =>
LiftedMeanResidual.fullResidual c s)
(m : ℕ)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal,
|w.1| ≤ 1 →
PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N →
w ∈ S →
‖iteratedFDeriv ℝ m (PhysicalResidualJetBounds.residual u P) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - PhysicalResidualJetBounds.physicalLoss h β m)
theorem
NavierStokes.ActualCycleResidualBounds.selected_residual_jetRate
{a b h gain β : ℝ}
{N Δ : ℕ}
{gap : ℕ → ℕ}
{U V : Set Cylinder}
{S : Set ProblemStatement.SpaceTime}
{c : CorrectionState.Context Point}
{s : CorrectionState.State Point}
{p₀ : ℕ → Cylinder → ℝ}
{u u₀ : ProblemStatement.VelocityField}
{P P₀ : ProblemStatement.PressureField}
(r : PhysicalResidualJetBounds.StateRealization h N gap U c s p₀ u P)
(g : SelectedGeometry a b h N Δ gap U V S)
(hh : 0 < h)
(hh1 : h < 1 / 2)
(ha : 0 < a)
(hN : 4 ≤ N)
(hf :
PhysicalResidualJetBounds.NativeBounds N V gain (fun (m : ℕ) => β * ↑m) fun (x : Unit) =>
LiftedMeanResidual.fullResidual c s)
(houtside :
∀ w ∈ PhysicalWaveSum.preterminal,
PhysicalWaveSum.physicalQ h w < ChartScales.Q N → w ∉ S → u =ᶠ[nhds w] u₀ ∧ P =ᶠ[nhds w] P₀)
(m : ℕ)
(hbase :
DiagonalResidual.JetRate (GlobalBaseError.originPast ⊓ Filter.principal Sᶜ) (PhysicalWaveSum.physicalQ h)
(PhysicalResidualJetBounds.residual u₀ P₀) m (gain - PhysicalResidualJetBounds.physicalLoss h β m))
:
Actual gap, given by ChartScales.nativeIndex ActualPrimary.h n - CommonWindow.index ActualPrimary.h n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Actual band graph, given by PhysicalResidualBridge.commonGraph (ChartScales.Q n) ActualPrimary.h (CommonWindow.index ActualPrimary.h n).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Actual base pressure, given by ActualBaseResidual.basePressure ActualPrimary.certificate ActualPrimary.modulation ActualPrimary.upper B n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
NavierStokes.ActualCycleResidualBounds.PhysicalFields
(B N : ℕ)
(U : Set Cylinder)
(s : CorrectionState.State Point)
(u : ProblemStatement.VelocityField)
(P : ProblemStatement.PressureField)
:
Only the actual physical realization remains external. Native regularity, the fixed base equation, and all size estimates are derived in this module.
- velocity_smooth (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (actualBandGraph n) U → ContDiffAt ℝ 2 u (z.1, CylindricalResidual.chart z.2)
- pressure_differentiable (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (actualBandGraph n) U → DifferentiableAt ℝ P (z.1, CylindricalResidual.chart z.2)
- velocity_germ (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (actualBandGraph n) U → (fun (y : ProblemStatement.SpaceTime) => u (y.1, CylindricalResidual.chart y.2)) =ᶠ[nhds z] fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (y.2.ofLp 1)) (PhysicalResidualTZ.velocityTZ (actualBandGraph n) (fun (v : PhysicalResidualTZ.Cylinder) (i : Fin 3) => PhysicalResidualBridge.baseComponents (CorrectionInitialization.ActualPrimary.commonContext B) n v i + PhysicalResidualBridge.incrementComponents s n v i) y)
- pressure_germ (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (actualBandGraph n) U → CylindricalResidual.pressurePullback P =ᶠ[nhds z] PhysicalResidualTZ.pressureTZ (actualBandGraph n) fun (v : PhysicalResidualTZ.Cylinder) => actualBasePressure B n v + s.totalPressureIncrement n v
- exterior (w : ProblemStatement.SpaceTime) : w ∈ PhysicalWaveSum.preterminal → PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w < ChartScales.Q N → w ∉ active → u w = FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w ∧ P w = FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w
Instances For
theorem
NavierStokes.ActualCycleResidualBounds.PhysicalFields.exterior_germs
{B N : ℕ}
{U : Set Cylinder}
{s : CorrectionState.State Point}
{u : ProblemStatement.VelocityField}
{P : ProblemStatement.PressureField}
(d : PhysicalFields B N U s u P)
{w : ProblemStatement.SpaceTime}
(hw : w ∈ PhysicalWaveSum.preterminal)
(hq : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w < ChartScales.Q N)
(hout : w ∉ active)
:
u =ᶠ[nhds w] FinalSlowBase.velocity CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B ∧ P =ᶠ[nhds w] FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate
CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B
Local exterior equality gives actual field germs inside the valid past sublevel; no global topological-support condition is used.
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.increment_smooth
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
{U : Set Cylinder}
(hU : ∀ z ∈ U, z.1 ∈ ActualInitialization.geometry.domain)
(n : ℕ)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤)
(fun (z : PhysicalResidualBridge.Cylinder) => PhysicalResidualBridge.incrementComponents x.state n z i) U
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.totalPressure_smooth
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
{U : Set Cylinder}
(hU : ∀ z ∈ U, z.1 ∈ ActualInitialization.geometry.domain)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (x.state.totalPressureIncrement n) U
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.stateRealization
{B N0 : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
{N : ℕ}
{U : Set Cylinder}
{u : ProblemStatement.VelocityField}
{P : ProblemStatement.PressureField}
(hopen : IsOpen U)
(hpos : ∀ z ∈ U, 0 < z.1.1)
(hdom : ∀ z ∈ U, z.1 ∈ ActualInitialization.geometry.domain)
(hbase : x.state.errors.base = ActualInitialization.baseError B)
(d : PhysicalFields B N U x.state u P)
:
The native operator and base-pressure obligations of the physical bridge are consequences of the actual selected base and the invariant.
Actual physical stage and iteration consumers #
theorem
NavierStokes.ActualCycleResidualBounds.actual_selectedGeometry
(N : ℕ)
:
SelectedGeometry ActualPolarCoverage.inner ActualPolarCoverage.outer CorrectionInitialization.ActualPrimary.h N
(CorrectionInitialization.CommonWindow.gap CorrectionInitialization.ActualPrimary.h) actualGap
ActualPolarCoverage.nativeDomain (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain) active
@[reducible, inline]
abbrev
NavierStokes.ActualCycleResidualBounds.PhysicalData
(B N : ℕ)
(s : CorrectionState.State Point)
(u : ProblemStatement.VelocityField)
(P : ProblemStatement.PressureField)
:
Physical data: an abbreviation for PhysicalFields B N ActualPolarCoverage.nativeDomain s u P.
Equations
Instances For
Fixed loss, given by physicalLoss ActualPrimary.h (2 * ActualPrimary.h) m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualCycleResidualBounds.Invariant.residual_jetRate
{B N0 N : ℕ}
{σ : ℝ}
{x : CorrectionStep.CycleState (Index B N0)}
(H : Invariant σ x)
{u : ProblemStatement.VelocityField}
{P : ProblemStatement.PressureField}
(hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hN : 4 ≤ N)
(hbase : x.state.errors.base = ActualInitialization.baseError B)
(d : PhysicalData B N x.state u P)
(m : ℕ)
:
The complete physical residual rate follows from the actual invariant.
The local physical fields are only identified, never bounded, by d.
theorem
NavierStokes.ActualCycleResidualBounds.initial_invariant
(B N0 : ℕ)
:
Invariant (1 / 5) (ActualInitialization.initialCycleState B N0)
theorem
NavierStokes.ActualCycleResidualBounds.finite_residual_rates
{B N0 N : ℕ}
(hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0)
(hN : 4 ≤ N)
(p : ℕ → CorrectionStep.CycleParameters (Index B N0))
(u : ℕ → ProblemStatement.VelocityField)
(P : ℕ → ProblemStatement.PressureField)
(H :
∀ (J : ℕ),
Invariant (ActualIterationLedger.sigma J)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) J))
(d :
∀ (J : ℕ),
PhysicalData B N
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) J).state
(u J) (P J))
(J m : ℕ)
:
DiagonalResidual.JetRate GlobalBaseError.originPast (PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h)
(fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (u J) (P J) w.1 w.2) m
(ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h J - fixedLoss m)
The finite-residual input of the mixed diagonal assembly. J is the
number of completed correction cycles, including the actual initialized
state at zero. The derivative loss is fixed before J is chosen.