Actual moving-strip bounds for the rank increment

The input is the measured slow debt. The rank coefficients are the explicit normalized coordinate formulas, and the output is the literal variable-gauge State increment. A fixed containing shell is used only to estimate the integral; the final class retains the original moving profile weight.

@[reducible, inline]

abbrev NavierStokes.RankStateBounds.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.RankStateBounds.Plane = NavierStokes.PressureStream.Plane

@[reducible, inline]

abbrev NavierStokes.RankStateBounds.Point : Type

Point: an abbreviation for MeanRankUpdate.ChartPoint /-! ## Lifting the actual slow debt -/.

Equations

• NavierStokes.RankStateBounds.Point = NavierStokes.MeanRankUpdate.ChartPoint

Lifting the actual slow debt

noncomputable def NavierStokes.RankStateBounds.slowProjection : Point →L[ℝ] Plane

Slow projection, given by (ContinuousLinearMap.fst ℝ Plane Plane).comp (ContinuousLinearMap.snd ℝ ℝ (Plane × Plane)).

Equations

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

theorem NavierStokes.RankStateBounds.norm_slowProjection_le : ‖slowProjection‖ ≤ 1

theorem NavierStokes.RankStateBounds.slowClass_lift {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (s : WeightedClasses.StripData Point) {U : Set Plane} (hU : IsOpen U) (hSU : ∀ x ∈ s.domain, x.2.1 ∈ U) {α : ℝ} {f : ℕ → Plane → F} (hf : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U hU s.epsilon s.slow ⋯ ⋯ ⋯) α f) : WeightedClasses.UnweightedClass s α fun (n : ℕ) (x : Point) => f n x.2.1

theorem NavierStokes.RankStateBounds.debtClass_of_components (s : WeightedClasses.StripData Plane) {α : ℝ} {d : ℕ → Plane → Fin 3 → ℝ} (hd : ∀ (i : Fin 3), WeightedClasses.UnweightedClass s α fun (n : ℕ) (x : Plane) => d n x i) : WeightedClasses.UnweightedClass s α d

Explicit normalized primitive data

structure NavierStokes.RankStateBounds.NormalizedParameters (coord A B : ℝ) (r : CorrectionState.RankData Plane) (U : Set Plane) : Prop

These are identities of input coefficients, not bounds on a constructed output.

• length (n : ℕ) (x : Plane) : x ∈ U → r.length n x = VariableGaugeMean.qLength coord x
• velocity (n : ℕ) (x : Plane) : x ∈ U → r.velocity n x = MeanRankUpdate.chartQ coord (0, x, 0) ^ (-A)
• coefficient (n : ℕ) (x : Plane) : x ∈ U → r.coefficient n x = MeanRankUpdate.shapedAmplitude B (MeanRankUpdate.chartEta coord (0, x, 0))

noncomputable def NavierStokes.RankStateBounds.normalizedData (coord A B lam a b : ℝ) : CorrectionState.RankData Plane

Normalized data, bundling lambda, inner, outer, length and the required compatibility proofs.

Equations

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

theorem NavierStokes.RankStateBounds.normalizedData_parameters (coord A B lam a b : ℝ) (U : Set Plane) : NormalizedParameters coord A B (normalizedData coord A B lam a b) U

theorem NavierStokes.RankStateBounds.NormalizedParameters.angular_eq {coord A B : ℝ} {r : CorrectionState.RankData Plane} {U : Set Plane} (h : NormalizedParameters coord A B r U) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) {z : Point} (hz : z.2.1 ∈ U) : MeanRankUpdate.slowLift (CorrectionState.rankAngular r c u n) z = MeanRankUpdate.chartAngular coord A B r.lambda r.inner r.outer (fun (x : MeanRankUpdate.ChartPoint) => CorrectionState.debt c u n x.2.1) z

theorem NavierStokes.RankStateBounds.NormalizedParameters.desired_eq {coord A B : ℝ} {r : CorrectionState.RankData Plane} {U : Set Plane} (h : NormalizedParameters coord A B r U) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) {z : Point} (hz : z.2.1 ∈ U) : MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n) z = MeanRankUpdate.chartAxial coord A B r.lambda r.inner r.outer (fun (x : MeanRankUpdate.ChartPoint) => CorrectionState.debt c u n x.2.1) z

A fixed shell used for intermediate estimates

theorem NavierStokes.RankStateBounds.containingShell {coord a b : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hab : a < b) : ∃ (lo : ℝ) (hi : ℝ), 0 < lo ∧ lo < hi ∧ lo < √U.qlo * a ∧ √U.qhi * b < hi ∧ (∀ x ∈ U.carrier, lo ≤ VariableGaugeMean.qLength coord x * a) ∧ ∀ x ∈ U.carrier, VariableGaugeMean.qLength coord x * b ≤ hi

theorem NavierStokes.RankStateBounds.fixed_weight_margin {lo hi a b qlo qhi cL cR : ℝ} (hlo : 0 < lo) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set Plane) (hU : IsOpen U) (hleft : lo < √qlo * a) (hright : √qhi * b < hi) : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ (PhysicalMeanDomain.localStripData lo hi cL cR hlo hcL hcR ε L hε hεone hL U hU).domain, p ∈ MeanRankUpdate.supportBand a b qlo qhi → δ ≤ (PhysicalMeanDomain.localStripData lo hi cL cR hlo hcL hcR ε L hε hεone hL U hU).zeta p

theorem NavierStokes.RankStateBounds.rankSources_fixedClass {coord A B cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) {g : VariableGaugeMean.GaugeData Plane} {r : CorrectionState.RankData Plane} {c : CorrectionState.Context Point} {u : CorrectionState.State Point} (hg : LocalRankDefect.RankGeometry g r U.carrier c u) (hparam : NormalizedParameters coord A B r U.carrier) (hB : B ≠ 0) {lo hi : ℝ} (hlo : 0 < lo) (hcL : 0 < cL) (hcR : 0 < cR) (hleft : lo < √U.qlo * r.inner) (hright : √U.qhi * r.outer < hi) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {H : ℝ} (hdebt : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H (CorrectionState.debt c u)) : (WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData lo hi cL cR hlo hcL hcR ε L hε hεone hL U.carrier ⋯) H fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankAngular r c u n)) ∧ WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData lo hi cL cR hlo hcL hcR ε L hε hεone hL U.carrier ⋯) H fun (n : ℕ) => MeanRankUpdate.slowLift (CorrectionState.rankDesiredAxial r c u n)

The source classes follow from the measured debt and the actual normalized rank inverse. Neither source class is a premise.

theorem NavierStokes.RankStateBounds.fixedClass_to_moving {coord a b inner outer lo hi cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (ha : 0 < a) (hlo : 0 < lo) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hleft : a < inner) (hright : outer < b) {H : ℝ} {f : ℕ → Point → ℝ} (hf : LocalRankDefect.LocalShell lo hi U.carrier f) (hs : ∀ (n : ℕ), VariableGaugeMean.SupportedGauge inner outer (VariableGaugeMean.qLength coord) U.carrier (f n)) (hclass : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData lo hi cL cR hlo hcL hcR ε L hε hεone hL U.carrier ⋯) H f) : WeightedClasses.MeanClass (LocalSignedRequest.movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) H f

The intermediate fixed shell is removed using actual reserved moving support and full local band jets.

theorem NavierStokes.RankStateBounds.rankIncrementState_bounds {coord A B cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (r : CorrectionState.RankData Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hg : LocalRankDefect.RankGeometry g r U.carrier c u) (hparam : NormalizedParameters coord A B r U.carrier) (hB : B ≠ 0) (hleft : g.radial.inner < r.inner) (hright : r.outer < g.radial.outer) (axial : Plane × Plane) {H : ℝ} (heps : WeightedClasses.BandBound (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.operators.epsilon) (hdebt : WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H (CorrectionState.debt c u)) : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.rankIncrementState g r axial c u)

The literal variable-gauge rank State update is bounded directly from the measured slow debt. The radial field gains its actual epsilon factor.

theorem NavierStokes.RankStateBounds.rankIncrementState_bounds_of_components {coord A B cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (r : CorrectionState.RankData Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hg : LocalRankDefect.RankGeometry g r U.carrier c u) (hparam : NormalizedParameters coord A B r U.carrier) (hB : B ≠ 0) (hleft : g.radial.inner < r.inner) (hright : r.outer < g.radial.outer) (axial : Plane × Plane) {H : ℝ} (heps : WeightedClasses.BandBound (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.operators.epsilon) (hdebt : ∀ (i : Fin 3), WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) H fun (n : ℕ) (x : LocalSignedRequest.Plane) => CorrectionState.debt c u n x i) : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.rankIncrementState g r axial c u)

theorem NavierStokes.RankStateBounds.rankIncrementState_bounds_of_defectBounds {coord A B cL cR : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (r : CorrectionState.RankData Plane) (ha : 0 < g.radial.inner) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hg : LocalRankDefect.RankGeometry g r U.carrier c u) (hparam : NormalizedParameters coord A B r U.carrier) (hB : B ≠ 0) (hleft : g.radial.inner < r.inner) (hright : r.outer < g.radial.outer) (axial : Plane × Plane) {σ H : ℝ} (hH : H ≤ 1 + σ) (heps : WeightedClasses.BandBound (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) 1 c.operators.epsilon) (hdebt : CorrectionState.DefectBounds (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) σ c u) : MeanIncrementBounds.IncrementBounds (LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) H (VariableGaugeMean.rankIncrementState g r axial c u)

theorem NavierStokes.RankStateBounds.rankIncrementState_support_margin {coord A B : ℝ} (U : LocalSignedRequest.SlowRegion coord) (g : VariableGaugeMean.GaugeData Plane) (r : CorrectionState.RankData Plane) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (hg : LocalRankDefect.RankGeometry g r U.carrier c u) (hparam : NormalizedParameters coord A B r U.carrier) (hleft : g.radial.inner < r.inner) (hright : r.outer < g.radial.outer) (axial : Plane × Plane) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (n : ℕ) (z : PressureStream.Lift Plane), z.2.1 ∈ U.carrier → (VariableGaugeMean.rankIncrementState g r axial c u).radial n z ≠ 0 ∨ (VariableGaugeMean.rankIncrementState g r axial c u).angular n z ≠ 0 ∨ (VariableGaugeMean.rankIncrementState g r axial c u).axial n z ≠ 0 → δ ≤ z.1 / VariableGaugeMean.qLength coord z.2.1 - g.radial.inner ∧ δ ≤ g.radial.outer - z.1 / VariableGaugeMean.qLength coord z.2.1

One positive profile margin controls every nonzero component of the actual rank increment, uniformly over bands and slow points.