Excluded errors of the actual initialized state

The base term is the normalized residual of the same fixed slow base. The primary Gaussian and current gauge aliases are retained literally.

Mean estimates for the chosen initial primary family

This module uses the literal primary choice, band labels, common gauge and rank data from CorrectionInitialization.ActualPrimary. In particular the stored base error is the actual base residual, whose angular continuity is used only on the positive-time domain.

@[reducible, inline]

abbrev NavierStokes.ActualInitialMean.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.ActualInitialMean.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.ActualInitialMean.Index (B N0 : ℕ) : Type

Index: an abbreviation for ActualPrimary.Label B N0 × Fin 2.

Equations

• NavierStokes.ActualInitialMean.Index B N0 = (NavierStokes.CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2)

noncomputable def NavierStokes.ActualInitialMean.strip : WeightedClasses.StripData Point

Strip, given by BaseContextAssembly.nativeStrip ActualPrimary.nominal ActualPrimary.standardRegion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.slowStrip : WeightedClasses.StripData TorusInverse.Plane

Slow strip, constructed using PhysicalMeanDomain.localSlowStripData.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.primaryPiece {B N0 : ℕ} (l : Index B N0) : CorrectionInitialization.PrimaryPiece (Point × ℝ)

Primary piece, given by ActualPrimary.piece ActualPrimary.standardRegion l.2 l.1.

Equations

• NavierStokes.ActualInitialMean.primaryPiece l = NavierStokes.CorrectionInitialization.ActualPrimary.piece NavierStokes.CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1

noncomputable def NavierStokes.ActualInitialMean.baseError (B : ℕ) : CorrectionState.Oscillation Point

Base error, given by ActualBaseResidual.baseError ActualPrimary.certificate ActualPrimary.modulation ActualPrimary.upper B.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.seed (B N0 : ℕ) : CorrectionState.State Point

Seed, given by bandSeed (ActualPrimary.activeLabels ActualPrimary.standardRegion B N0) primaryPiece (baseError B).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.axial : TorusInverse.Plane × TorusInverse.Plane

Axial, given by ((0, 1), 0).

Equations

• NavierStokes.ActualInitialMean.axial = ((0, 1), 0)

noncomputable def NavierStokes.ActualInitialMean.primary (B N0 : ℕ) : CorrectionState.State Point

Primary, given by VariableGaugeMean.reconstructState ActualPrimary.commonGauge (ActualPrimary.commonContext B) (seed B N0).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.temporal (B N0 : ℕ) : CorrectionState.State Point

Temporal, constructed using VariableGaugeMean.temporalStageState.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.ranked (B N0 : ℕ) : CorrectionState.State Point

Ranked, constructed using VariableGaugeMean.rankStageState.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.initialized (B N0 : ℕ) : CorrectionState.State Point

Initialized, constructed using GaugeInitialization.initializedBands.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.initialAlias (B N0 n : ℕ) (x : Point) : Fin 3 → ℝ

Initial alias, constructed using VariableGaugeMean.temporalAliasState.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialMean.phase {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) : ℝ

Phase, given by (primaryPiece l).coefficients.phase n (x, 0).

Equations

• NavierStokes.ActualInitialMean.phase l n x = (NavierStokes.ActualInitialMean.primaryPiece l).coefficients.phase n (x, 0)

noncomputable def NavierStokes.ActualInitialMean.angularMode {B N0 : ℕ} (l : Index B N0) (_n : ℕ) : ℤ

Angular mode, constructed using PrimaryGeometryAssembly.angularMode.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialMean.angularMode_ne_zero {B N0 : ℕ} (l : Index B N0) (n : ℕ) : angularMode l n ≠ 0

theorem NavierStokes.ActualInitialMean.phase_split {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) (theta : ℝ) : (primaryPiece l).coefficients.frequency n * (primaryPiece l).coefficients.phase n (x, theta) = (primaryPiece l).coefficients.frequency n * phase l n x + ↑(angularMode l n) * theta

theorem NavierStokes.ActualInitialMean.cutoff_smooth {B N0 : ℕ} (l : Index B N0) (n : ℕ) : ContDiff ℝ (↑⊤) ((primaryPiece l).cutoff n)

theorem NavierStokes.ActualInitialMean.amplitude_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent (primaryPiece l).coefficients.amplitude

theorem NavierStokes.ActualInitialMean.cutoff_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent (primaryPiece l).cutoff

theorem NavierStokes.ActualInitialMean.exact_amplitude_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent (primaryPiece l).exactCoefficients.amplitude

theorem NavierStokes.ActualInitialMean.tangent_amplitude_angle {B N0 : ℕ} (l : Index B N0) : ErrorHarmonics.AngleIndependent ((primaryPiece l).coefficients.withCutoff (primaryPiece l).cutoff).amplitude

theorem NavierStokes.ActualInitialMean.gaussian_mean_zero {B N0 : ℕ} (l : Index B N0) : CorrectionStep.angularMeanVector (primaryPiece l).excluded = 0

theorem NavierStokes.ActualInitialMean.gaussian_angularContinuous {B N0 : ℕ} (l : Index B N0) : CorrectionStep.AngularContinuous (primaryPiece l).excluded

theorem NavierStokes.ActualInitialMean.meanGoodResidual_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (n : ℕ) (x : D) (i : Fin 3) (hb : Continuous fun (theta : ℝ) => u.errors.base n (x, theta) i) (hg : Continuous fun (theta : ℝ) => u.errors.gaussian n (x, theta) i) (ha : Continuous fun (theta : ℝ) => u.errors.aliasError n (x, theta) i) : u.meanGoodResidual c n x i = (u.reducedMeanResidual c n x i - HarmonicResidual.realAngularMean fun (theta : ℝ) => u.errors.gaussian n (x, theta) i) - HarmonicResidual.realAngularMean fun (theta : ℝ) => u.errors.aliasError n (x, theta) i

Only continuity along the single angular integration fiber is needed.

theorem NavierStokes.ActualInitialMean.initialized_meanGood (B N0 n : ℕ) {x : Point} (hT : 0 < x.2.1.1) (i : Fin 3) : (initialized B N0).meanGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x i = (initialized B N0).reducedMeanResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x i - initialAlias B N0 n x i

noncomputable def NavierStokes.ActualInitialMean.envelope {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) : ℝ

Envelope, given by ActualPrimaryBounds.fullEnvelope (l.2, l.1) n (x, 0).

Equations

• NavierStokes.ActualInitialMean.envelope l n x = NavierStokes.ActualPrimaryBounds.fullEnvelope (l.2, l.1) n (x, 0)

theorem NavierStokes.ActualInitialMean.envelope_nonneg {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) : 0 ≤ envelope l n x

theorem NavierStokes.ActualInitialMean.envelope_le_one {B N0 : ℕ} (l : Index B N0) (n : ℕ) (x : Point) : envelope l n x ≤ 1

theorem NavierStokes.ActualInitialMean.tangent_amplitude_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass strip envelope (1 / 2) fun (l : Index B N0) (n : ℕ) (x : Point) => ((primaryPiece l).coefficients.withCutoff (primaryPiece l).cutoff).amplitude n (x, 0)

theorem NavierStokes.ActualInitialMean.seed_angularSmooth (B N0 : ℕ) : WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) (seed B N0).oscillation

theorem NavierStokes.ActualInitialMean.seed_covariance_smooth (B N0 : ℕ) (i j : Fin 3) : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) ((seed B N0).covariance i j)

theorem NavierStokes.ActualInitialMean.tangent_angularSmooth (B N0 : ℕ) : WaveStateRegularity.AngularSmooth (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) (ActualPrimaryCovariance.tangentSum B N0)

theorem NavierStokes.ActualInitialMean.tangent_covariance_smooth (B N0 : ℕ) (i j : Fin 3) : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) (ActualPrimaryCovariance.tangentCovariance B N0 i j)

theorem NavierStokes.ActualInitialMean.seed_waveSupport (B N0 : ℕ) : WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (seed B N0).oscillation

theorem NavierStokes.ActualInitialMean.seed_covariance_regular (B N0 : ℕ) (i j : Fin 3) : GaugeDebtIncrement.Regular CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer ((seed B N0).covariance i j)

theorem NavierStokes.ActualInitialMean.active_index_le {B N0 n : ℕ} {l : Index B N0} (hl : l ∈ CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0 n) : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.1)

theorem NavierStokes.ActualInitialMean.seed_velocity_periodic (B N0 n : ℕ) (R : ℝ) (s : TorusInverse.Plane) (theta : ℝ) : FourierAlias.TorusPeriodic fun (Y : TorusInverse.Plane) => (seed B N0).oscillation n ((R, s, Y), theta)

theorem NavierStokes.ActualInitialMean.covariance_periodic_of_periodic {U : Set TorusInverse.Plane} {u : CorrectionState.Oscillation Point} (hu : ∀ (n : ℕ) (theta : ℝ) (i : Fin 3), PhysicalMeanDomain.PeriodicOn U fun (x : PressureStream.Lift TorusInverse.Plane) => u n (x, theta) i) (i j : Fin 3) (n : ℕ) : PhysicalMeanDomain.PeriodicOn U (CorrectionState.bilinearCovariance u u i j n)

theorem NavierStokes.ActualInitialMean.seed_covariance_periodic (B N0 : ℕ) (i j : Fin 3) (n : ℕ) : PhysicalMeanDomain.PeriodicOn CorrectionInitialization.ActualPrimary.standardRegion.carrier ((seed B N0).covariance i j n)

theorem NavierStokes.ActualInitialMean.covariance_bounds_of_curl (B N0 : ℕ) (hc : LabelSumBounds.UniformWaveClass strip envelope (1 - ChartScales.kappa) fun (l : Index B N0) (n : ℕ) (x : Point) => ((primaryPiece l).coefficients.withCutoff (primaryPiece l).cutoff).curlCorrection (primaryPiece l).strip (primaryPiece l).directions n (x, 0)) : (∀ (i j : Fin 3), WeightedClasses.MeanClass strip 1 ((seed B N0).covariance i j)) ∧ ∀ (i j : Fin 3), WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) ((seed B N0).covariance i j - ActualPrimaryCovariance.tangentCovariance B N0 i j)

The estimate comes from actual cut amplitudes, curl corrections and closed slot supports. Its constants do not count the growing label set.

theorem NavierStokes.ActualInitialMean.meanBar_mem {alpha : ℝ} {f : CorrectionState.ScalarField Point} (hf : MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) f) (hclass : WeightedClasses.MeanClass strip alpha f) : WeightedClasses.MeanClass strip alpha (StateMomentBalances.meanBar f)

theorem NavierStokes.ActualInitialMean.matched_fluxes_of_covariance (B N0 : ℕ) (hr : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) ((seed B N0).covariance i j)) (ht : ∀ (i j : Fin 3), MeanIncrementBounds.SmoothOn (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) (ActualPrimaryCovariance.tangentCovariance B N0 i j)) (hc : ∀ (i j : Fin 3), WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) ((seed B N0).covariance i j - ActualPrimaryCovariance.tangentCovariance B N0 i j)) : WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((seed B N0).covariance 0 1) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualTheta) ∧ WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((seed B N0).covariance 0 2) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualAxial)

The fixed base and the actual common index supply all the non-primary fields of the initialization estimates.

noncomputable def NavierStokes.ActualInitialMean.PrimaryData (B N0 : ℕ) : Prop

Primary data, constructed using MovingInitialization.PrimaryMeanData.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialMean.movingSupport_supportedGauge {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) {f : Point → ℝ} (hs : LocalSignedRequest.MovingSupport a b coord U.carrier f) : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) U.carrier f

theorem NavierStokes.ActualInitialMean.primaryData_of_covariance (B N0 : ℕ) (hc : ∀ (i j : Fin 3), WeightedClasses.MeanClass strip 1 ((seed B N0).covariance i j)) (hr : ∀ (i j : Fin 3), GaugeDebtIncrement.Regular CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer ((seed B N0).covariance i j)) (hp : ∀ (i j : Fin 3) (n : ℕ), PhysicalMeanDomain.PeriodicOn CorrectionInitialization.ActualPrimary.standardRegion.carrier ((seed B N0).covariance i j n)) : PrimaryData B N0

theorem NavierStokes.ActualInitialMean.initialized_mean_bounds_of_rank (B N0 : ℕ) {sigma : ℝ} (htheta : WeightedClasses.MeanClass strip (1 + sigma) ((ranked B N0).thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (haxial : WeightedClasses.MeanClass strip (1 + sigma) fun (n : ℕ) (x : Point) => (ranked B N0).axialResidual (CorrectionInitialization.ActualPrimary.commonContext B) n x - VariableGaugeMean.temporalAliasState CorrectionInitialization.ActualPrimary.commonGauge CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.commonContext B) (primary B N0) n (x, 0) 2) : CorrectionState.MeanResidualBounds strip sigma (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0)

theorem NavierStokes.ActualInitialMean.initial_bounds_of_primaryData (B N0 : ℕ) (d : PrimaryData B N0) (htheta : WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((seed B N0).covariance 0 1) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualTheta)) (haxial : WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((seed B N0).covariance 0 2) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualAxial)) : CorrectionState.CumulativeBounds strip (initialized B N0) ∧ CorrectionState.MeanResidualBounds strip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0) ∧ CorrectionState.DefectBounds slowStrip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0) ∧ GaugeMassPreservation.ZeroMassesOn CorrectionInitialization.ActualPrimary.standardRegion.carrier (initialized B N0)

Unconditional bounds for the chosen family

theorem NavierStokes.ActualInitialMean.curl_amplitude_uniform {B N0 : ℕ} : LabelSumBounds.UniformWaveClass strip envelope (1 - ChartScales.kappa) fun (l : Index B N0) (n : ℕ) (x : Point) => ((primaryPiece l).coefficients.withCutoff (primaryPiece l).cutoff).curlCorrection (primaryPiece l).strip (primaryPiece l).directions n (x, 0)

theorem NavierStokes.ActualInitialMean.covariance_bounds (B N0 : ℕ) : (∀ (i j : Fin 3), WeightedClasses.MeanClass strip 1 ((seed B N0).covariance i j)) ∧ ∀ (i j : Fin 3), WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) ((seed B N0).covariance i j - ActualPrimaryCovariance.tangentCovariance B N0 i j)

theorem NavierStokes.ActualInitialMean.primary_mean_data (B N0 : ℕ) : PrimaryData B N0

Every field is supplied by the actual primary family and fixed base.

theorem NavierStokes.ActualInitialMean.primary_bounds (B N0 : ℕ) : WeightedClasses.MeanClass strip (1 - ChartScales.kappa) ((primary B N0).gr (CorrectionInitialization.ActualPrimary.commonContext B)) ∧ WeightedClasses.MeanClass strip (1 - ChartScales.kappa) (primary B N0).pressure ∧ WeightedClasses.MeanClass strip (1 - ChartScales.kappa) ((primary B N0).thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B)) ∧ WeightedClasses.MeanClass strip (1 - ChartScales.kappa) ((primary B N0).axialResidual (CorrectionInitialization.ActualPrimary.commonContext B)) ∧ CorrectionState.CumulativeBounds strip (primary B N0)

theorem NavierStokes.ActualInitialMean.matched_fluxes (B N0 : ℕ) : WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((seed B N0).covariance 0 1) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualTheta) ∧ WeightedClasses.MeanClass strip (3 / 2 - ChartScales.kappa) (StateMomentBalances.meanBar ((seed B N0).covariance 0 2) - StateMomentBalances.meanBar (CorrectionInitialization.ActualPrimary.commonContext B).virtualAxial)

theorem NavierStokes.ActualInitialMean.temporal_bounds (B N0 : ℕ) : CorrectionInitialization.MovingInitialization.TemporalStateBounds CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge ⋯ ⋯ ⋯ (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h) BaseContextAssembly.slowScale ⋯ ⋯ BaseContextAssembly.one_le_slowScale CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) axial (CorrectionInitialization.ActualPrimary.commonContext B) (seed B N0)

theorem NavierStokes.ActualInitialMean.rank_bounds (B N0 : ℕ) : CorrectionInitialization.MovingInitialization.InitialRankBounds CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge ⋯ ⋯ ⋯ (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h) BaseContextAssembly.slowScale ⋯ ⋯ BaseContextAssembly.one_le_slowScale CorrectionInitialization.ActualPrimary.rankData CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) axial (CorrectionInitialization.ActualPrimary.commonContext B) (seed B N0)

theorem NavierStokes.ActualInitialMean.initial_bounds (B N0 : ℕ) : CorrectionState.CumulativeBounds strip (initialized B N0) ∧ CorrectionState.MeanResidualBounds strip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0) ∧ CorrectionState.DefectBounds slowStrip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0) ∧ GaugeMassPreservation.ZeroMassesOn CorrectionInitialization.ActualPrimary.standardRegion.carrier (initialized B N0)

All bands of the literal initialization, with the two aliases retained.

theorem NavierStokes.ActualInitialMean.initial_cumulative_bounds (B N0 : ℕ) : CorrectionState.CumulativeBounds strip (initialized B N0)

theorem NavierStokes.ActualInitialMean.initial_mean_bounds (B N0 : ℕ) : CorrectionState.MeanResidualBounds strip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0)

theorem NavierStokes.ActualInitialMean.initial_debt_bounds (B N0 : ℕ) : CorrectionState.DefectBounds slowStrip (1 / 5) (CorrectionInitialization.ActualPrimary.commonContext B) (initialized B N0)

theorem NavierStokes.ActualInitialMean.initial_zeroMasses (B N0 : ℕ) : GaugeMassPreservation.ZeroMassesOn CorrectionInitialization.ActualPrimary.standardRegion.carrier (initialized B N0)

theorem NavierStokes.ActualInitialMean.initial_mean_smooth (B N0 : ℕ) : MeanIncrementBounds.SmoothTriple (PhysicalMeanDomain.slowDomain CorrectionInitialization.ActualPrimary.standardRegion.carrier) (initialized B N0).mean

theorem NavierStokes.ActualInitialMean.initial_mean_support (B N0 : ℕ) : CorrectionStep.GaugeSupportedTriple CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (VariableGaugeMean.qLength (2 * CorrectionInitialization.ActualPrimary.h)) CorrectionInitialization.ActualPrimary.standardRegion.carrier (initialized B N0).mean

theorem NavierStokes.ActualInitialMean.initialized_formula (B N0 : ℕ) : initialized B N0 = CorrectionInitialization.GaugeInitialization.initializedBands CorrectionInitialization.ActualPrimary.commonGauge CorrectionInitialization.ActualPrimary.rankData CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) ((0, 1), 0) (CorrectionInitialization.ActualPrimary.commonContext B) (CorrectionInitialization.ActualPrimary.activeLabels CorrectionInitialization.ActualPrimary.standardRegion B N0) (fun (l : CorrectionInitialization.ActualPrimary.Label B N0 × Fin 2) => CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion l.2 l.1) (ActualBaseResidual.baseError CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B)

theorem NavierStokes.ActualInitialExcluded.radialDivergence_contDiffAt {f : SimilarityProfile.PhysicalProfile} {p : SimilarityProfile.PhysicalPoint} (hf : ContDiffAt ℝ (↑⊤) f p) (hs : 0 < p.2.1) (k : ℝ) : ContDiffAt ℝ (↑⊤) (LeadingStress.radialDivergence k f) p

theorem NavierStokes.ActualInitialExcluded.stressForce_contDiffAt {f g : SimilarityProfile.PhysicalProfile} {z : ProblemStatement.SpaceTime} (hf : ContDiffAt ℝ (↑⊤) f (AxisymmetricFields.profilePoint z.1 z.2)) (hg : ContDiffAt ℝ (↑⊤) g (AxisymmetricFields.profilePoint z.1 z.2)) (hr : 0 < AxisymmetricFields.radialEnergy z.2) : ContDiffAt ℝ (↑⊤) (BaseResidual.stressForce f g) z

theorem NavierStokes.ActualInitialExcluded.stressForce_congr {f g f' g' : SimilarityProfile.PhysicalProfile} {z : ProblemStatement.SpaceTime} (hf : f =ᶠ[nhds (AxisymmetricFields.profilePoint z.1 z.2)] f') (hg : g =ᶠ[nhds (AxisymmetricFields.profilePoint z.1 z.2)] g') : BaseResidual.stressForce f g z = BaseResidual.stressForce f' g' z

noncomputable def NavierStokes.ActualInitialExcluded.continuationDomain (h : ℝ) : Set ProblemStatement.SpaceTime

Continuation domain, given by EndpointCoordinates.cartesianDomain h ∩ {z | 0 < AxisymmetricFields.radialEnergy z.2}.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.continuationDomain_open (h : ℝ) : IsOpen (continuationDomain h)

noncomputable def NavierStokes.ActualInitialExcluded.baseErrorContinuation {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.SpaceTime → ProblemStatement.Space

The original profiles and original scale schedule continued through the regular endpoint coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.baseErrorContinuation_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (baseErrorContinuation H v upper B) (continuationDomain F.data.h)

theorem NavierStokes.ActualInitialExcluded.baseErrorContinuation_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : baseErrorContinuation H v upper B z = FinalSlowBase.error H v upper B z

theorem NavierStokes.ActualInitialExcluded.baseErrorContinuation_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : baseErrorContinuation H v upper B =ᶠ[nhds z] FinalSlowBase.error H v upper B

@[reducible, inline]

abbrev NavierStokes.ActualInitialExcluded.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.ActualInitialExcluded.Slow = NavierStokes.PhaseCalculus.Slow

noncomputable def NavierStokes.ActualInitialExcluded.closedSlowSet {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : Set Slow

A compact closed set containing the native slow region. Its last inequality retains separation from the simultaneous time/axial origin.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.closedSlowSet_compact {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : IsCompact (closedSlowSet W U)

theorem NavierStokes.ActualInitialExcluded.slowCarrier_subset_closedSlowSet {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : BaseContextAssembly.slowCarrier W U ⊆ closedSlowSet W U

theorem NavierStokes.ActualInitialExcluded.closedSlowSet_radius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {p : Slow} (hp : p ∈ closedSlowSet W U) : 0 < p.1

theorem NavierStokes.ActualInitialExcluded.closedSlowSet_axial_ne {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {p : Slow} (hp : p ∈ closedSlowSet W U) (hT : p.2.2 = 0) : p.2.1 ≠ 0

noncomputable def NavierStokes.ActualInitialExcluded.bandLinear (h Q : ℝ) : Slow →L[ℝ] ProblemStatement.SpaceTime

Band linear as an element of Slow →L[ℝ] SpaceTime.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.bandPoint_affine (h Q : ℝ) (p : Slow) : BaseChartJets.bandPoint h Q p = (bandLinear h Q) p + (1, 0)

theorem NavierStokes.ActualInitialExcluded.bandPoint_smooth (h Q : ℝ) : ContDiff ℝ (↑⊤) (BaseChartJets.bandPoint h Q)

theorem NavierStokes.ActualInitialExcluded.bandPoint_closed_mem {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {Q : ℝ} (hQ : 0 < Q) {p : Slow} (hp : p ∈ closedSlowSet W U) : BaseChartJets.bandPoint F.data.h Q p ∈ continuationDomain F.data.h

theorem NavierStokes.ActualInitialExcluded.bandLinear_bound {h Q : ℝ} (hQ : 0 < Q) (hQone : Q ≤ 1) (hD : 0 ≤ CoordinateAlgebra.D h) : ‖bandLinear h Q‖ ≤ 4

theorem NavierStokes.ActualInitialExcluded.Q_tendsto_zero : Filter.Tendsto ChartScales.Q Filter.atTop (nhds 0)

noncomputable def NavierStokes.ActualInitialExcluded.nativeApproachFilter {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : Filter ProblemStatement.SpaceTime

Native approach filter, constructed using Filter.map.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.nativeApproach_q_bound {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {n : ℕ} {p : Slow} (hp : p ∈ BaseContextAssembly.slowCarrier W U) : 0 < (SlowBorelBase.cartesianChart F.data.h (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)).1 ∧ (SlowBorelBase.cartesianChart F.data.h (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)).1 ≤ ChartScales.Q n * U.qhi

noncomputable def NavierStokes.ActualInitialExcluded.nativeApproach {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : BaseResidual.PhysicalApproach (nativeApproachFilter W U) F.data.h 0 (NominalConeAssembly.activeRight W)

Native approach, bundling carrier, compact, in_carrier, exact and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.physical_error_eventual {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) (r : ℝ) (hr : 0 ≤ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ p ∈ BaseContextAssembly.slowCarrier W U, ‖iteratedFDeriv ℝ m (FinalSlowBase.error H v upper B) (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)‖ ≤ C * ChartScales.Q n ^ r

theorem NavierStokes.ActualInitialExcluded.physical_error_fixed {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ p ∈ BaseContextAssembly.slowCarrier W U, ‖iteratedFDeriv ℝ m (FinalSlowBase.error H v upper B) (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)‖ ≤ C

Fixed bands include the nonzero-axial terminal boundary. Their compact bound comes from the actual continuation, not an open-past box.

theorem NavierStokes.ActualInitialExcluded.physical_error_jet_bound {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) (r : ℝ) (hr : 0 ≤ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), ∀ p ∈ BaseContextAssembly.slowCarrier W U, ‖iteratedFDeriv ℝ m (FinalSlowBase.error H v upper B) (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)‖ ≤ C * ChartScales.Q n ^ r

theorem NavierStokes.ActualInitialExcluded.physical_error_prefix_bound {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) (r : ℝ) (hr : 0 ≤ r) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), ∀ p ∈ BaseContextAssembly.slowCarrier W U, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (FinalSlowBase.error H v upper B) (BaseChartJets.bandPoint F.data.h (ChartScales.Q n) p)‖ ≤ C * ChartScales.Q n ^ r

noncomputable def NavierStokes.ActualInitialExcluded.normalizedBase {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (p : Slow) : ProblemStatement.Space

Normalized base, constructed using ChartScales.Q.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.normalizedBase_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (n : ℕ) : ContDiffOn ℝ (↑⊤) (normalizedBase H v upper B n) (BaseContextAssembly.slowCarrier W U)

theorem NavierStokes.ActualInitialExcluded.normalizedBase_prefix {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (alpha : ℝ) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), ∀ p ∈ BaseContextAssembly.slowCarrier W U, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (normalizedBase H v upper B n) p‖ ≤ C * ChartScales.epsilon F.data.h n ^ alpha

theorem NavierStokes.ActualInitialExcluded.normalizedBase_envelope {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (alpha : ℝ) : PrimaryPulseBounds.EnvelopeJets (BaseChartJets.unitScale (BaseContextAssembly.phaseDomain W U ℕ)) (fun (n : ℕ) (x : BaseContextAssembly.Slow) => ChartScales.epsilon F.data.h n ^ alpha) (normalizedBase H v upper B)

theorem NavierStokes.ActualInitialExcluded.baseError_zero_angle {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B n : ℕ) (x : BaseContextAssembly.Point) (i : Fin 3) : ActualBaseResidual.baseError H v upper B n (x, 0) i = (normalizedBase H v upper B n (BaseContextAssembly.slowCoordinates x)).ofLp i

theorem NavierStokes.ActualInitialExcluded.baseError_component_class {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (alpha : ℝ) (i : Fin 3) : WeightedClasses.UnweightedClass (BaseContextAssembly.nativeStrip W U) alpha fun (n : ℕ) (x : BaseContextAssembly.Point) => ActualBaseResidual.baseError H v upper B n (x, 0) i

Every actual base-error component has all powers on the full free auxiliary lift. No vanishing edge-weight premise is imposed on this term.

theorem NavierStokes.ActualInitialExcluded.baseError_angle_component_class {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (alpha : ℝ) (i : Fin 3) : WeightedClasses.UnweightedClass (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip W U)) alpha fun (n : ℕ) (x : BaseContextAssembly.Point × ℝ) => ActualBaseResidual.baseError H v upper B n x i

noncomputable def NavierStokes.ActualInitialExcluded.nativeGaussian {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (x : ActualPrimaryBounds.Native) : HarmonicCalculus.ComplexVector

The genuine fast derivative of the Gaussian cutoff, multiplied by the actual attached primary solution.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.nativeGaussian_jets {B N0 : ℕ} : PrimaryCopyBounds.NativeJets (PrimaryCopyBounds.signDomain (NativeBandExtension.radialDomain CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared)) (ActualPrimaryBounds.nativeWeight (1 / 2)) nativeGaussian

theorem NavierStokes.ActualInitialExcluded.nativeGaussian_core {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (x : ActualPrimaryBounds.Native) (hx : nativeGaussian l x ≠ 0) : x.2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.ActualInitialExcluded.nativeGaussian_zero_plateau {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) {x : ActualPrimaryBounds.Native} (hx : |x.2.2 / (CorrectionInitialization.ActualPrimary.phases B N0 0).L l.2 - 1 / 2| < 1 / 5) : nativeGaussian l =ᶠ[nhds x] fun (x : ActualPrimaryBounds.Native) => 0

noncomputable def NavierStokes.ActualInitialExcluded.nativeBandScales : GaussianTailFlat.BandScaleControl ActualPrimaryBounds.nativeStrip

Native band scales, bundling power, epsilon_eq, boundConstant, constant_one_le and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ActualInitialExcluded.gaussianLengthLower : ℝ

Gaussian length lower, given by 2 * ActualPrimary.slots.radius / 25.

Equations

• NavierStokes.ActualInitialExcluded.gaussianLengthLower = 2 * NavierStokes.CorrectionInitialization.ActualPrimary.slots.radius / 25

theorem NavierStokes.ActualInitialExcluded.gaussianLengthLower_pos : 0 < gaussianLengthLower

theorem NavierStokes.ActualInitialExcluded.gaussianLength_near {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (hn : ActualPrimaryBounds.near l n) : gaussianLengthLower * ChartScales.S n ≤ (CorrectionInitialization.ActualPrimary.phases B N0 0).L l.2

noncomputable def NavierStokes.ActualInitialExcluded.gaussianLength {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : ℝ

Outside the active finite band window the copied field is identically zero. The auxiliary length merely makes the global index bookkeeping total.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.gaussianLength_pos {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : 0 < gaussianLength l n

theorem NavierStokes.ActualInitialExcluded.gaussianLength_eq {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (hn : ActualPrimaryBounds.near l n) : gaussianLength l n = (CorrectionInitialization.ActualPrimary.phases B N0 0).L l.2

noncomputable def NavierStokes.ActualInitialExcluded.gaussianRate (B N0 : ℕ) : ℝ

Gaussian rate, given by ActualGaussianCoverage.gaussianRate (ActualPrimary.choice B N0).prepared.M⁻¹ (ActualPrimary.choice B N0).prepared.u.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.gaussianRate_pos (B N0 : ℕ) : 0 < gaussianRate B N0

theorem NavierStokes.ActualInitialExcluded.nativeEnvelope_gaussian {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) {v : ℝ} (hv : v ∈ Set.Icc 0 ((CorrectionInitialization.ActualPrimary.phases B N0 0).L l.2)) : ActualPrimaryBounds.pulseEnvelope l v ≤ Real.exp (-gaussianRate B N0 * (v / (CorrectionInitialization.ActualPrimary.phases B N0 0).L l.2 - 1 / 2) ^ 2 * (CorrectionInitialization.ActualPrimary.phases B N0 0).L l.2)

theorem NavierStokes.ActualInitialExcluded.copiedGaussian_all_gains {B N0 : ℕ} (a β : ℝ) : PeriodizedWaveBounds.UniformLocalJets ActualPrimaryBounds.nativeStrip (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Native) => √(ActualPrimaryBounds.nativeStrip.zeta x_2)) β (fun (l : ActualPrimaryBounds.SignedLabel B N0) => (ActualPrimaryBounds.copyCells l).carrier) (ActualPrimaryBounds.copied a nativeGaussian)

Uniform Gaussian gain before restoring the angular carrier. The moving edge factor remains sqrt(zeta) at every requested exponent.

theorem NavierStokes.ActualInitialExcluded.periodizedGaussian_all_gains {B N0 : ℕ} (a β : ℝ) : LabelSumBounds.UniformClass ActualPrimaryBounds.nativeStrip (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Native) => √(ActualPrimaryBounds.nativeStrip.zeta x_2)) β (ActualPrimaryBounds.periodized a nativeGaussian)

noncomputable def NavierStokes.ActualInitialExcluded.labelCarrier {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : Set ActualPrimaryBounds.Point

The original label's actual slow mask and Gaussian source rectangle, on the common torus lift. The harmonic index does not change this set.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.labelCarrier_closed {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : IsClosed (labelCarrier l n)

theorem NavierStokes.ActualInitialExcluded.nativeGaussian_source_support {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : Function.support (nativeGaussian l) ⊆ ActualGaussianCoverage.actualSourceCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2

theorem NavierStokes.ActualInitialExcluded.nativeGaussian_source_tsupport {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : tsupport (nativeGaussian l) ⊆ ActualGaussianCoverage.actualSourceCore CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation (CorrectionInitialization.ActualPrimary.choice B N0).prepared l.2

noncomputable def NavierStokes.ActualInitialExcluded.chartGaussian {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : ℕ → CorrectionInitialization.ActualPrimary.FullPoint → HarmonicCalculus.ComplexVector

Chart gaussian, constructed using LinearWaveBounds.excludedSlotError.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.nativeGaussian_smooth {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiff ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.gaussian L)

theorem NavierStokes.ActualInitialExcluded.chartCutoff_germ {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : (ActualPrimaryDynamics.copyPoint l.1 l.2 n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2 n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => CorrectionInitialization.ActualPrimary.gaussian l.2 (ActualPrimaryDynamics.copyPoint l.1 l.2 n k y)

theorem NavierStokes.ActualInitialExcluded.fast_nativeGaussian {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (fderiv ℝ (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => CorrectionInitialization.ActualPrimary.gaussian l.2 (ActualPrimaryDynamics.copyPoint l.1 l.2 n k y)) x) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n x) = ActualPrimaryDynamics.clockScale l.2 n * (fderiv ℝ (CorrectionInitialization.ActualPrimary.gaussian l.2) (ActualPrimaryDynamics.copyPoint l.1 l.2 n k x)) (0, 0, 1)

theorem NavierStokes.ActualInitialExcluded.gaussianScale_eq {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : ActualPrimaryDynamics.clockScale l.2 n * ActualPrimaryDynamics.velocityScale l.2 n = ActualPrimaryBounds.coefficientScale (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 1 / 2) l n

theorem NavierStokes.ActualInitialExcluded.chartGaussian_germ {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : (ActualPrimaryDynamics.copyPoint l.1 l.2 n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : chartGaussian l n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ActualPrimaryBounds.coefficientScale (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 1 / 2) l n • nativeGaussian l (ActualPrimaryDynamics.copyPoint l.1 l.2 n k y)

theorem NavierStokes.ActualInitialExcluded.chartGaussian_zero_no_copy {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : ∀ (k : TorusInverse.Frequency), (ActualPrimaryDynamics.copyPoint l.1 l.2 n k x).2 ∉ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : chartGaussian l n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

theorem NavierStokes.ActualInitialExcluded.chartGaussian_support {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : Function.support (chartGaussian l n) ⊆ Prod.fst ⁻¹' labelCarrier l n

theorem NavierStokes.ActualInitialExcluded.chartGaussian_zero_germ {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x.1 ∉ labelCarrier l n) : chartGaussian l n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

theorem NavierStokes.ActualInitialExcluded.dynamics_copyPoint_eq {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (hn : ActualPrimaryBounds.near l n) (k : TorusInverse.Frequency) (x : ActualPrimaryBounds.Native) (θ : ℝ) : ActualPrimaryDynamics.copyPoint l.1 l.2 n k (ActualSignedGeometry.meanEquiv x, θ) = ActualPrimaryBounds.copyPoint l n k x

theorem NavierStokes.ActualInitialExcluded.periodizedGaussian_eq {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : ActualPrimaryBounds.Native} (hx : x ∈ ActualPrimaryBounds.nativeStrip.domain) (θ : ℝ) : ActualPrimaryBounds.periodized (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h + 1 / 2) nativeGaussian l n x = chartGaussian l n (ActualSignedGeometry.meanEquiv x, θ)

theorem NavierStokes.ActualInitialExcluded.chartGaussian_all_gains {B N0 : ℕ} (β : ℝ) : LabelSumBounds.UniformClass (HarmonicWaveInteraction.productStrip ActualPrimaryBounds.strip) (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point × ℝ) => √(ActualPrimaryBounds.strip.zeta x_2.1)) β chartGaussian

The actual initialized Gaussian coefficient, uniformly in every label and on the entire free auxiliary and angular lift.

theorem NavierStokes.ActualInitialExcluded.gaussianCoefficient_all_gains {B N0 : ℕ} (β : ℝ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformClass ActualPrimaryBounds.strip (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : ActualPrimaryBounds.Point) => √(ActualPrimaryBounds.strip.zeta x_2)) β fun (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (x : ActualPrimaryBounds.Point) => (ErrorHarmonics.conjugatePair 1 fun (y : LocalSignedRequest.Point) => chartGaussian l n (y, 0) i).coeff j x

theorem NavierStokes.ActualInitialExcluded.gaussianCoefficient_zero {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (i : Fin 3) (j : ℤ) {x : ActualPrimaryBounds.Point} (hx : x ∉ labelCarrier l n) : (ErrorHarmonics.conjugatePair 1 fun (y : LocalSignedRequest.Point) => chartGaussian l n (y, 0) i).coeff j x = 0

theorem NavierStokes.ActualInitialExcluded.gaussianCoefficient_support {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (i : Fin 3) : HarmonicSourceSupport.NonzeroSupported (labelCarrier l n) (ErrorHarmonics.conjugatePair 1 fun (y : ActualPrimaryBounds.Point) => chartGaussian l n (y, 0) i)

theorem NavierStokes.ActualInitialExcluded.uniform_flat_mul {D : Type} {I : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : I → ℕ → D → ℝ} {K : I → ℕ → Set D} {f g : I → ℕ → D → ℂ} (hf : ∀ (α : ℝ), LabelSumBounds.UniformClass s w α f) (hg : ∀ (i : I) (n : ℕ), ContDiffOn ℝ (↑⊤) (g i n) s.domain) (hz : ∀ (i : I) (n : ℕ), ∀ x ∈ s.domain, x ∉ K i n → f i n =ᶠ[nhds x] fun (x : D) => 0) (hb : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ) (r : ℝ), ∀ (i : I) (n : ℕ), ∀ x ∈ s.domain, x ∈ K i n → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (g i n) x‖ ≤ WeightedClasses.majorant s (fun (x : ℕ) (x_1 : D) => 1) r C p n x) (β : ℝ) : LabelSumBounds.UniformClass s w β fun (i : I) (n : ℕ) (x : D) => f i n x * g i n x

Only carrier jets on the actual coefficient support are used. Their fixed-order loss is absorbed by the independently proved all-power input.

@[reducible, inline]

noncomputable abbrev NavierStokes.ActualInitialExcluded.gaussianStrip : WeightedClasses.StripData CorrectionInitialization.ActualPrimary.FullPoint

Gaussian strip: an abbreviation for HarmonicWaveInteraction.productStrip strip.

Equations

• NavierStokes.ActualInitialExcluded.gaussianStrip = NavierStokes.HarmonicWaveInteraction.productStrip NavierStokes.ActualPrimaryBounds.strip

noncomputable def NavierStokes.ActualInitialExcluded.chartCarrier {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint → ℂ

Chart carrier, constructed using HarmonicCalculus.carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.chartCarrier_smooth {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (chartCarrier l n) gaussianStrip.domain

noncomputable def NavierStokes.ActualInitialExcluded.gaussianField {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) : ℕ → CorrectionInitialization.ActualPrimary.FullPoint → Fin 3 → ℝ

Gaussian field, given by (ActualPrimary.piece ActualPrimary.standardRegion l.1 l.2).excluded.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.gaussianField_eq {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) (i : Fin 3) : gaussianField l n x i = (chartGaussian l n x i * HarmonicCalculus.carrier ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).frequency n) ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).phase n) x).re

theorem NavierStokes.ActualInitialExcluded.chartGaussian_cut_support {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : chartGaussian l n x ≠ 0) : x ∈ Function.support (((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2)).amplitude n)

theorem NavierStokes.ActualInitialExcluded.chartGaussian_zero_off_cut {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∉ tsupport (((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2)).amplitude n)) : chartGaussian l n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

theorem NavierStokes.ActualInitialExcluded.gaussianField_window {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ gaussianStrip.domain) (i : Fin 3) (hn : gaussianField l n x i ≠ 0) : ActualPrimaryCovariance.physicalWindow n x.1 ∈ LabelSumBounds.closedWindow (CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h) (ActualPrimaryCovariance.signedLabelOf (l.2, l.1))

theorem NavierStokes.ActualInitialExcluded.gaussianField_zero_germ {B N0 : ℕ} (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (i : Fin 3) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x.1 ∉ labelCarrier l n) : (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => gaussianField l n y i) =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

theorem NavierStokes.ActualInitialExcluded.gaussianField_all_gains_of_carrier {B N0 : ℕ} (hc : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ) (r : ℝ), ∀ (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ), ∀ x ∈ gaussianStrip.domain, x ∈ tsupport (((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff l.1 l.2)).amplitude n) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (HarmonicCalculus.carrier ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).frequency n) ((CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).phase n)) x‖ ≤ WeightedClasses.majorant gaussianStrip (fun (x : ℕ) (x_1 : CorrectionInitialization.ActualPrimary.FullPoint) => 1) r C p n x) (β : ℝ) (i : Fin 3) : LabelSumBounds.UniformClass gaussianStrip (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : CorrectionInitialization.ActualPrimary.FullPoint) => √(ActualPrimaryBounds.strip.zeta x_2.1)) β fun (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => gaussianField l n x i

noncomputable def NavierStokes.ActualInitialExcluded.initialGaussian (B N0 : ℕ) : ℕ → CorrectionInitialization.ActualPrimary.FullPoint → Fin 3 → ℝ

Initial gaussian, constructed using LabelSumBounds.fieldSum.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ActualInitialExcluded.initialGaussian_class_of_fields {B N0 : ℕ} (β : ℝ) (i : Fin 3) (hf : LabelSumBounds.UniformClass gaussianStrip (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : CorrectionInitialization.ActualPrimary.FullPoint) => √(ActualPrimaryBounds.strip.zeta x_2.1)) β fun (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => gaussianField l n x i) : WeightedClasses.MemClass gaussianStrip (fun (x : ℕ) (x_1 : CorrectionInitialization.ActualPrimary.FullPoint) => √(ActualPrimaryBounds.strip.zeta x_1.1)) β fun (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => initialGaussian B N0 n x i

The number of active labels may grow, but at most the fixed geometric overlap number contributes to an actual derivative at one point.

theorem NavierStokes.ActualInitialExcluded.strip_zeta_le_one (x : ActualPrimaryBounds.Point) : ActualPrimaryBounds.strip.zeta x ≤ 1

theorem NavierStokes.ActualInitialExcluded.initialGaussian_unweighted_of_fields {B N0 : ℕ} (β : ℝ) (i : Fin 3) (hf : LabelSumBounds.UniformClass gaussianStrip (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : CorrectionInitialization.ActualPrimary.FullPoint) => √(ActualPrimaryBounds.strip.zeta x_2.1)) β fun (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => gaussianField l n x i) : WeightedClasses.UnweightedClass gaussianStrip β fun (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => initialGaussian B N0 n x i

theorem NavierStokes.ActualInitialExcluded.primary_axial_class {B N0 : ℕ} (d : ActualInitialMean.PrimaryData B N0) : WeightedClasses.MeanClass ActualPrimaryBounds.strip (1 - ChartScales.kappa) ((ActualInitialMean.primary B N0).axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))

theorem NavierStokes.ActualInitialExcluded.temporalAlias_all_gains_of_primaryData {B N0 : ℕ} (d : ActualInitialMean.PrimaryData B N0) (β : ℝ) : (WeightedClasses.MeanClass ActualPrimaryBounds.strip β fun (n : ℕ) (x : ActualPrimaryBounds.Point) => VariableGaugeMean.temporalAliasState CorrectionInitialization.ActualPrimary.commonGauge CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialMean.primary B N0) n (x, 0)) ∧ WeightedClasses.MeanClass gaussianStrip β (VariableGaugeMean.temporalAliasState CorrectionInitialization.ActualPrimary.commonGauge CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialMean.primary B N0))

theorem NavierStokes.ActualInitialExcluded.pressureAlias_all_gains_of_cumulative {B N0 : ℕ} (d : ActualInitialMean.PrimaryData B N0) (hu : CorrectionState.CumulativeBounds ActualPrimaryBounds.strip (ActualInitialMean.ranked B N0)) (β : ℝ) : (WeightedClasses.MeanClass ActualPrimaryBounds.strip β fun (n : ℕ) (x : ActualPrimaryBounds.Point) => VariableGaugeMean.pressureAliasState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialMean.ranked B N0) n (x, 0)) ∧ WeightedClasses.MeanClass gaussianStrip β (VariableGaugeMean.pressureAliasState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialMean.ranked B N0))

theorem NavierStokes.ActualInitialExcluded.initialAlias_all_gains_of_data {B N0 : ℕ} (d : ActualInitialMean.PrimaryData B N0) (hu : CorrectionState.CumulativeBounds ActualPrimaryBounds.strip (ActualInitialMean.ranked B N0)) (β : ℝ) : WeightedClasses.MeanClass ActualPrimaryBounds.strip β (ActualInitialMean.initialAlias B N0)

theorem NavierStokes.ActualInitialExcluded.initialAlias_all_gains (B N0 : ℕ) (β : ℝ) : WeightedClasses.MeanClass ActualPrimaryBounds.strip β (ActualInitialMean.initialAlias B N0)

The two actual gauge aliases of the initialized state, with no quantitative input assumptions on a residual or an alias.

theorem NavierStokes.ActualInitialExcluded.initializedAlias_all_gains (B N0 : ℕ) (β : ℝ) : WeightedClasses.MeanClass gaussianStrip β (ActualInitialMean.initialized B N0).errors.aliasError

theorem NavierStokes.ActualInitialExcluded.initializedAlias_unweighted (B N0 : ℕ) (β : ℝ) : WeightedClasses.UnweightedClass gaussianStrip β (ActualInitialMean.initialized B N0).errors.aliasError

theorem NavierStokes.ActualInitialExcluded.initialized_errors_formula (B N0 : ℕ) : (ActualInitialMean.initialized B N0).errors.total = ActualBaseResidual.baseError CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B + initialGaussian B N0 + (ActualInitialMean.initialized B N0).errors.aliasError

theorem NavierStokes.ActualInitialExcluded.initializedErrors_all_gains_of_gaussian (B N0 : ℕ) (β : ℝ) (i : Fin 3) (hg : WeightedClasses.UnweightedClass gaussianStrip β fun (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => initialGaussian B N0 n x i) : WeightedClasses.UnweightedClass gaussianStrip β fun (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => (ActualInitialMean.initialized B N0).errors.total n x i

The remaining Gaussian premise is an estimate for the literal full field; the base and both aliases in this formula are already constructed.

theorem NavierStokes.ActualInitialExcluded.gaussianField_all_gains (B N0 : ℕ) (β : ℝ) (i : Fin 3) : LabelSumBounds.UniformClass gaussianStrip (fun (x : ActualPrimaryBounds.SignedLabel B N0) (x_1 : ℕ) (x_2 : CorrectionInitialization.ActualPrimary.FullPoint) => √(ActualPrimaryBounds.strip.zeta x_2.1)) β fun (l : ActualPrimaryBounds.SignedLabel B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => gaussianField l n x i

All actual derivatives of the restored primary Gaussian field retain the flat edge weight, uniformly over the whole label family.

theorem NavierStokes.ActualInitialExcluded.initialGaussian_all_gains (B N0 : ℕ) (β : ℝ) (i : Fin 3) : WeightedClasses.MemClass gaussianStrip (fun (x : ℕ) (x_1 : CorrectionInitialization.ActualPrimary.FullPoint) => √(ActualPrimaryBounds.strip.zeta x_1.1)) β fun (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => initialGaussian B N0 n x i

theorem NavierStokes.ActualInitialExcluded.initialGaussian_unweighted (B N0 : ℕ) (β : ℝ) (i : Fin 3) : WeightedClasses.UnweightedClass gaussianStrip β fun (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => initialGaussian B N0 n x i

theorem NavierStokes.ActualInitialExcluded.initializedErrors_all_gains (B N0 : ℕ) (β : ℝ) (i : Fin 3) : WeightedClasses.UnweightedClass gaussianStrip β fun (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) => (ActualInitialMean.initialized B N0).errors.total n x i

The actual full excluded error of the literal initialized state has every positive power (indeed every real power), on the whole angular and free auxiliary lift. There is no supplied output-bound premise.

theorem NavierStokes.ActualInitialExcluded.initializedErrors_vector_all_gains (B N0 : ℕ) (β : ℝ) : WeightedClasses.UnweightedClass gaussianStrip β (ActualInitialMean.initialized B N0).errors.total