Every-power bounds for the literal cycle's axisymmetric alias

The three newly evaluated aliases use one fixed similarity gauge, strip, covering index, and fast operator. Their bounds are derived from primitive state regularity and ordinary cumulative/covariance estimates.

@[reducible, inline]

abbrev NavierStokes.ActualCycleExcluded.Point : Type

Point: an abbreviation for MeanStateRegularity.Point.

Equations

• NavierStokes.ActualCycleExcluded.Point = NavierStokes.MeanStateRegularity.Point

structure NavierStokes.ActualCycleExcluded.SimilarityData : Type

Fixed numerical and geometric data for the actual similarity estimates.

• h : ℝ

  Step-size parameter of SimilarityData, of type ℝ.

• h_pos : 0 < self.h
• inner : ℝ

  Inner of SimilarityData, of type ℝ.

• outer : ℝ

  Outer of SimilarityData, of type ℝ.

• inner_pos : 0 < self.inner
• inner_lt_outer : self.inner < self.outer
• leftWeight : ℝ

  Left weight of SimilarityData, of type ℝ.

• rightWeight : ℝ

  Right weight of SimilarityData, of type ℝ.

• left_pos : 0 < self.leftWeight
• right_pos : 0 < self.rightWeight
• baseScale : ℝ

  Base scale of SimilarityData, of type ℝ.

• baseScale_ne : self.baseScale ≠ 0
• region : LocalSignedRequest.SlowRegion (2 * self.h)

  Region of SimilarityData, of type SlowRegion (2 * h).

• index : ℕ → ℕ

  Index of SimilarityData, of type ℕ → ℕ.

• gap : ℕ

  Gap of SimilarityData, of type ℕ.

• index_lower (n : ℕ) : ChartScales.nativeIndex self.h n ≤ self.index n + self.gap
• index_upper (n : ℕ) : self.index n ≤ ChartScales.nativeIndex self.h n + self.gap
• slow : ℕ → ℝ

  Slow of SimilarityData, of type ℕ → ℝ.

• slow_one (n : ℕ) : 1 ≤ self.slow n
• slow_scale (n : ℕ) : ChartScales.S n ≤ self.slow n

noncomputable def NavierStokes.ActualCycleExcluded.SimilarityData.strip (d : SimilarityData) : WeightedClasses.StripData Point

Strip, given by GaugeExcludedBounds.actualStrip (b := d.outer) d.region d.inner_pos d.left_pos d.right_pos d.h_pos d.slow d.slow_one.

Equations

• d.strip = NavierStokes.GaugeExcludedBounds.actualStrip d.region ⋯ ⋯ ⋯ ⋯ d.slow ⋯

noncomputable def NavierStokes.ActualCycleExcluded.SimilarityData.gauge (d : SimilarityData) : VariableGaugeMean.GaugeData TorusInverse.Plane

Gauge, given by GaugeExcludedBounds.actualGauge d.h d.inner d.outer d.baseScale d.inner_lt_outer d.index.

Equations

• d.gauge = NavierStokes.GaugeExcludedBounds.actualGauge d.h d.inner d.outer d.baseScale ⋯ d.index

structure NavierStokes.ActualCycleExcluded.Compatible {ι : Type} (d : SimilarityData) (p : CorrectionStep.CycleParameters ι) (c : CorrectionState.Context Point) : Prop

These are equalities of the actual data used by the cycle, not hypotheses on any excluded output field.

• gauge : p.gauge = d.gauge
• strip : p.strip = d.strip
• time : p.timeExponent = d.h
• index : p.commonIndex = d.index
• fast : c.operators.fastCoefficient = fun (n : ℕ) => ChartScales.Tg ^ d.index n * ChartScales.Q n ^ (1 + d.h)
• temporal : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal)

theorem NavierStokes.ActualCycleExcluded.stage_primitives {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {coord : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < p.gauge.radial.inner) (hd : 0 < p.gauge.radial.exponent) (hell : ∀ (n : ℕ), p.gauge.length n = VariableGaugeMean.qLength coord) (H : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c u) (hX₁ : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField U p.gauge.radial.inner p.gauge.radial.outer (SignedMeanGain.covarianceIncrement u.oscillation (p.particularVelocity v c u) i j)) (hX₂ : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField U p.gauge.radial.inner p.gauge.radial.outer (SignedMeanGain.covarianceIncrement (p.afterParticular v c u).oscillation (p.signedVelocity v c u) i j)) (hrank : LocalRankDefect.RankGeometry p.gauge p.rank U.carrier c u) : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c (p.afterSigned v c u) ∧ MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c (p.afterRank v c u)

Regularity of the two states at which the new aliases are evaluated. The original rank geometry is reused after recomputing the actual debt.

theorem NavierStokes.ActualCycleExcluded.afterRank_cumulative_of_next {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {s : WeightedClasses.StripData Point} (hnext : CorrectionState.CumulativeBounds s (p.next v c u)) : CorrectionState.CumulativeBounds s (p.afterRank v c u)

theorem NavierStokes.ActualCycleExcluded.afterRank_covariance_mem {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {s : WeightedClasses.StripData Point} {γ : ℝ} (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass s γ (u.covariance i j)) (hX₁ : ∀ (i j : Fin 3), WeightedClasses.MeanClass s γ (SignedMeanGain.covarianceIncrement u.oscillation (p.particularVelocity v c u) i j)) (hX₂ : ∀ (i j : Fin 3), WeightedClasses.MeanClass s γ (SignedMeanGain.covarianceIncrement (p.afterParticular v c u).oscillation (p.signedVelocity v c u) i j)) (i j : Fin 3) : WeightedClasses.MeanClass s γ ((p.afterRank v c u).covariance i j)

The covariance is updated only by the two actual wave increments. Temporal and rank mean changes leave this covariance unchanged.

theorem NavierStokes.ActualCycleExcluded.nextAxisymmetricAlias_eq {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (axis : CorrectionStep.AxisymmetricAlias) : p.nextAxisymmetricAlias v c u axis = (axis + fun (n : ℕ) (x : PressureStream.Lift PressureStream.Plane) => VariableGaugeMean.temporalAliasState p.gauge p.timeExponent p.commonIndex c (p.afterSigned v c u) n (x, 0)) + ((fun (n : ℕ) (x : PressureStream.Lift PressureStream.Plane) => VariableGaugeMean.pressureAliasState p.gauge c (p.afterRank v c u) n (x, 0)) - fun (n : ℕ) (x : PressureStream.Lift PressureStream.Plane) => VariableGaugeMean.pressureAliasState p.gauge c u n (x, 0))

theorem NavierStokes.ActualCycleExcluded.nextAxisymmetricAlias_all_powers {ι : Type} (d : SimilarityData) (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (matchData : Compatible d p c) {κ α γ : ℝ} (H : MeanStateRegularity.PrimitiveData d.region d.inner d.outer c u) (hX₁ : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField d.region d.inner d.outer (SignedMeanGain.covarianceIncrement u.oscillation (p.particularVelocity v c u) i j)) (hX₂ : ∀ (i j : Fin 3), GaugeMomentBalances.MovingField d.region d.inner d.outer (SignedMeanGain.covarianceIncrement (p.afterParticular v c u).oscillation (p.signedVelocity v c u) i j)) (hrank : LocalRankDefect.RankGeometry p.gauge p.rank d.region.carrier c u) (ho : MeanIncrementBounds.OperatorBounds p.strip c.operators κ) (hb : MeanIncrementBounds.BaseBounds p.strip c.base) (hu : CorrectionState.CumulativeBounds p.strip u) (hnext : CorrectionState.CumulativeBounds p.strip (p.next v c u)) (hW : ∀ (i j : Fin 3), WeightedClasses.MeanClass p.strip γ (u.covariance i j)) (hCov₁ : ∀ (i j : Fin 3), WeightedClasses.MeanClass p.strip γ (SignedMeanGain.covarianceIncrement u.oscillation (p.particularVelocity v c u) i j)) (hCov₂ : ∀ (i j : Fin 3), WeightedClasses.MeanClass p.strip γ (SignedMeanGain.covarianceIncrement (p.afterParticular v c u).oscillation (p.signedVelocity v c u) i j)) (hraw : WeightedClasses.MeanClass p.strip α ((p.afterSigned v c u).axialResidual c)) (axis : CorrectionStep.AxisymmetricAlias) (haxis : ∀ (β : ℝ), WeightedClasses.MeanClass p.strip β axis) (β : ℝ) : WeightedClasses.MeanClass p.strip β (p.nextAxisymmetricAlias v c u axis)

The three new aliases are estimated by GaugeExcludedBounds for the same concrete similarity data. The after-signed and after-rank primitive certificates are derived, and the old pressure alias is subtracted.