Changes of the literal mean equations under an actual mean increment

The differential operators below are genuine graph derivatives. The nonlinear fields are the products in equation (32), including every old/new mean cross term. The unchanged wave covariance and virtual flux cancel only after an exact residual-difference identity.

@[reducible, inline]

abbrev NavierStokes.MeanIncrementBounds.Field (D : Type) : Type

Field: an abbreviation for ℕ → D → ℝ.

Equations

• NavierStokes.MeanIncrementBounds.Field D = (ℕ → D → ℝ)

structure NavierStokes.MeanIncrementBounds.Triple (D : Type) : Type

Triple data, collecting radial, angular, axial.

• radial : Field D

  Radial of Triple, of type Field D.

• angular : Field D

  Angular of Triple, of type Field D.

• axial : Field D

  Axial of Triple, of type Field D.

noncomputable def NavierStokes.MeanIncrementBounds.updated {D : Type} (m h : Triple D) : Triple D

Updated, given by ⟨m.radial + h.radial, m.angular + h.angular, m.axial + h.axial⟩.

Equations

• NavierStokes.MeanIncrementBounds.updated m h = { radial := m.radial + h.radial, angular := m.angular + h.angular, axial := m.axial + h.axial }

structure NavierStokes.MeanIncrementBounds.Operators (D : Type) : Type

Operators data, collecting epsilon, radialFrequency, fastCoefficient, radius, radialProfile, eR and their compatibility conditions.

• epsilon : ℕ → ℝ

  The smallness parameter at each stage.

• radialFrequency : ℕ → ℝ

  Radial frequency of Operators, of type ℕ → ℝ.

• fastCoefficient : ℕ → ℝ

  Fast coefficient of Operators, of type ℕ → ℝ.

• radius : D → ℝ

  Radius of Operators, of type D → ℝ.

• radialProfile : D → ℝ

  Radial profile of Operators, of type D → ℝ.

• eR : D

  E R of Operators, of type D.

• eZ : D

  E Z of Operators, of type D.

• eT : D

  E T of Operators, of type D.

• vR : D

  V R of Operators, of type D.

• vT : D

  V T of Operators, of type D.

noncomputable def NavierStokes.MeanIncrementBounds.Operators.invRadius {D : Type} (o : Operators D) : Field D

Inv radius, defined pointwise by (o.radius x)⁻¹.

Equations

• o.invRadius x✝ x = (o.radius x)⁻¹

noncomputable def NavierStokes.MeanIncrementBounds.Operators.dr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (f : Field D) : Field D

Dr, given by graphDerivative o.radialFrequency o.radialProfile o.eR o.vR f.

Equations

• o.dr f = NavierStokes.WeightedClasses.graphDerivative o.radialFrequency o.radialProfile o.eR o.vR f

noncomputable def NavierStokes.MeanIncrementBounds.Operators.dz {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (f : Field D) : Field D

Dz, defined pointwise by o.epsilon n * fderiv ℝ (f n) x o.eZ.

Equations

• o.dz f n x = o.epsilon n * (fderiv ℝ (f n) x) o.eZ

noncomputable def NavierStokes.MeanIncrementBounds.Operators.slowTime {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (f : Field D) : Field D

Slow time, defined pointwise by -(o.epsilon n * fderiv ℝ (f n) x o.eT).

Equations

• o.slowTime f n x = -(o.epsilon n * (fderiv ℝ (f n) x) o.eT)

noncomputable def NavierStokes.MeanIncrementBounds.Operators.fastTime {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (f : Field D) : Field D

Fast time, defined pointwise by o.fastCoefficient n * fderiv ℝ (f n) x o.vT.

Equations

• o.fastTime f n x = o.fastCoefficient n * (fderiv ℝ (f n) x) o.vT

noncomputable def NavierStokes.MeanIncrementBounds.Operators.time {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (f : Field D) : Field D

Time, given by o.slowTime f + o.fastTime f.

Equations

• o.time f = o.slowTime f + o.fastTime f

noncomputable def NavierStokes.MeanIncrementBounds.Operators.radialDiv {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (c : ℝ) (f : Field D) : Field D

Radial div, given by o.dr f + c • (o.invRadius * f).

Equations

• o.radialDiv c f = o.dr f + c • (o.invRadius * f)

noncomputable def NavierStokes.MeanIncrementBounds.Operators.viscosity {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (c : ℝ) (f : Field D) : Field D

The connection parameter is one for radial/angular velocity, zero axially.

Equations

• o.viscosity c f n x = o.epsilon n * (o.dr (o.dr f) n x + o.invRadius n x * o.dr f n x + o.dz (o.dz f) n x - c * (o.invRadius n x * (o.invRadius n x * f n x)))

def NavierStokes.MeanIncrementBounds.SmoothOn {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : Set D) (f : Field D) : Prop

Smooth on, given by ∀ n, ContDiffOn ℝ ∞ (f n) U.

Equations

• NavierStokes.MeanIncrementBounds.SmoothOn U f = ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) U

def NavierStokes.MeanIncrementBounds.Agree {D : Type} (U : Set D) (f g : Field D) : Prop

Agree, given by ∀ n, EqOn (f n) (g n) U.

Equations

• NavierStokes.MeanIncrementBounds.Agree U f g = ∀ (n : ℕ), Set.EqOn (f n) (g n) U

theorem NavierStokes.MeanIncrementBounds.SmoothOn.add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : SmoothOn U (f + g)

theorem NavierStokes.MeanIncrementBounds.SmoothOn.mul {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : SmoothOn U (f * g)

theorem NavierStokes.MeanIncrementBounds.SmoothOn.neg {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : Field D} (hf : SmoothOn U f) : SmoothOn U (-f)

theorem NavierStokes.MeanIncrementBounds.SmoothOn.sub {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : SmoothOn U (f - g)

theorem NavierStokes.MeanIncrementBounds.SmoothOn.smul {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : Field D} (hf : SmoothOn U f) (c : ℝ) : SmoothOn U (c • f)

theorem NavierStokes.MeanIncrementBounds.SmoothOn.directional {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : Field D} (hf : SmoothOn U f) (hU : IsOpen U) (v : D) : SmoothOn U fun (n : ℕ) (x : D) => (fderiv ℝ (f n) x) v

theorem NavierStokes.MeanIncrementBounds.SmoothOn.at_point {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : Field D} (hf : SmoothOn U f) (hU : IsOpen U) (n : ℕ) {x : D} (hx : x ∈ U) : ContDiffAt ℝ (↑⊤) (f n) x

theorem NavierStokes.MeanIncrementBounds.SmoothOn.dr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : Field D} (hf : SmoothOn U f) (hU : IsOpen U) (o : Operators D) (ha : ContDiffOn ℝ (↑⊤) o.radialProfile U) : SmoothOn U (o.dr f)

theorem NavierStokes.MeanIncrementBounds.SmoothOn.dz {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : Field D} (hf : SmoothOn U f) (hU : IsOpen U) (o : Operators D) : SmoothOn U (o.dz f)

theorem NavierStokes.MeanIncrementBounds.agree_fderiv {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {f g : Field D} (h : Agree U f g) (n : ℕ) {x : D} (hx : x ∈ U) : fderiv ℝ (f n) x = fderiv ℝ (g n) x

theorem NavierStokes.MeanIncrementBounds.class_congr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : Field D} (hf : WeightedClasses.MemClass s w α f) (h : Agree s.domain g f) : WeightedClasses.MemClass s w α g

theorem NavierStokes.MeanIncrementBounds.Operators.dr_congr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) {f g : Field D} (h : Agree U f g) : Agree U (o.dr f) (o.dr g)

theorem NavierStokes.MeanIncrementBounds.Operators.dr_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : Agree U (o.dr (f + g)) (o.dr f + o.dr g)

theorem NavierStokes.MeanIncrementBounds.Operators.dz_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : Agree U (o.dz (f + g)) (o.dz f + o.dz g)

theorem NavierStokes.MeanIncrementBounds.Operators.dz_congr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) {f g : Field D} (h : Agree U f g) : Agree U (o.dz f) (o.dz g)

theorem NavierStokes.MeanIncrementBounds.Operators.time_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : Agree U (o.time (f + g)) (o.time f + o.time g)

theorem NavierStokes.MeanIncrementBounds.Operators.radialDiv_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) (c : ℝ) {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : Agree U (o.radialDiv c (f + g)) (o.radialDiv c f + o.radialDiv c g)

theorem NavierStokes.MeanIncrementBounds.Operators.viscosity_add {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) (ha : ContDiffOn ℝ (↑⊤) o.radialProfile U) (c : ℝ) {f g : Field D} (hf : SmoothOn U f) (hg : SmoothOn U g) : Agree U (o.viscosity c (f + g)) (o.viscosity c f + o.viscosity c g)

structure NavierStokes.MeanIncrementBounds.OperatorBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (o : Operators D) (κ : ℝ) : Prop

Operator bounds data, collecting epsilon_eq, radialProfile, invRadius, radialFrequency, fastCoefficient, kappa_nonneg and their compatibility conditions.

• epsilon_eq : o.epsilon = s.epsilon
• radialProfile : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) => o.radialProfile
• invRadius : WeightedClasses.UnweightedClass s 0 o.invRadius
• radialFrequency : WeightedClasses.BandBound s (-κ) o.radialFrequency
• fastCoefficient : WeightedClasses.BandBound s 0 o.fastCoefficient
• kappa_nonneg : 0 ≤ κ
• weight_le_one (x : D) : x ∈ s.domain → s.zeta x ≤ 1

theorem NavierStokes.MeanIncrementBounds.Class.neg {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α : ℝ} {f : Field D} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s α (-f)

theorem NavierStokes.MeanIncrementBounds.Class.sub {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α : ℝ} {f g : Field D} (hf : WeightedClasses.MeanClass s α f) (hg : WeightedClasses.MeanClass s α g) : WeightedClasses.MeanClass s α (f - g)

theorem NavierStokes.MeanIncrementBounds.Class.smul {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α : ℝ} {f : Field D} (hf : WeightedClasses.MeanClass s α f) (c : ℝ) : WeightedClasses.MeanClass s α (c • f)

theorem NavierStokes.MeanIncrementBounds.Class.product {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α β : ℝ} {f g : Field D} (hf : WeightedClasses.MeanClass s α f) (hg : WeightedClasses.MeanClass s β g) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) : WeightedClasses.MeanClass s (α + β) (f * g)

theorem NavierStokes.MeanIncrementBounds.Class.coefficient_mul {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α β : ℝ} {f g : Field D} (hf : WeightedClasses.UnweightedClass s α f) (hg : WeightedClasses.MeanClass s β g) : WeightedClasses.MeanClass s (α + β) (f * g)

theorem NavierStokes.MeanIncrementBounds.Class.mul_coefficient {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α β : ℝ} {f g : Field D} (hf : WeightedClasses.MeanClass s α f) (hg : WeightedClasses.UnweightedClass s β g) : WeightedClasses.MeanClass s (α + β) (f * g)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.epsilon {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ : ℝ} (ho : OperatorBounds s o κ) : WeightedClasses.BandBound s 1 o.epsilon

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.dr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s (α - κ) (o.dr f)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.dz {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s (α + 1) (o.dz f)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.slowTime {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s (α + 1) (o.slowTime f)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.fastTime {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s α (o.fastTime f)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.time {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s α (o.time f)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.inv_mul {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) : WeightedClasses.MeanClass s α (o.invRadius * f)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.radialDiv {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) (c : ℝ) : WeightedClasses.MeanClass s (α - κ) (o.radialDiv c f)

theorem NavierStokes.MeanIncrementBounds.OperatorBounds.viscosity {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ α : ℝ} (ho : OperatorBounds s o κ) {f : Field D} (hf : WeightedClasses.MeanClass s α f) (c : ℝ) : WeightedClasses.MeanClass s (α + 1 - 2 * κ) (o.viscosity c f)

noncomputable def NavierStokes.MeanIncrementBounds.thetaRadial {D : Type} (b m : Triple D) : Field D

Theta radial, given by b.radial * m.angular + m.radial * b.angular + m.radial * m.angular.

Equations

• NavierStokes.MeanIncrementBounds.thetaRadial b m = b.radial * m.angular + m.radial * b.angular + m.radial * m.angular

noncomputable def NavierStokes.MeanIncrementBounds.thetaAxial {D : Type} (b m : Triple D) : Field D

Theta axial, given by b.axial * m.angular + b.angular * m.axial + m.axial * m.angular.

Equations

• NavierStokes.MeanIncrementBounds.thetaAxial b m = b.axial * m.angular + b.angular * m.axial + m.axial * m.angular

noncomputable def NavierStokes.MeanIncrementBounds.axialRadial {D : Type} (b m : Triple D) : Field D

Axial radial, given by b.radial * m.axial + m.radial * b.axial + m.radial * m.axial.

Equations

• NavierStokes.MeanIncrementBounds.axialRadial b m = b.radial * m.axial + m.radial * b.axial + m.radial * m.axial

noncomputable def NavierStokes.MeanIncrementBounds.axialAxial {D : Type} (b m : Triple D) : Field D

Axial axial, given by (2 : ℝ) • (b.axial * m.axial) + m.axial * m.axial.

Equations

• NavierStokes.MeanIncrementBounds.axialAxial b m = 2 • (b.axial * m.axial) + m.axial * m.axial

noncomputable def NavierStokes.MeanIncrementBounds.radialRadial {D : Type} (b m : Triple D) : Field D

Radial radial, given by (2 : ℝ) • (b.radial * m.radial) + m.radial * m.radial.

Equations

• NavierStokes.MeanIncrementBounds.radialRadial b m = 2 • (b.radial * m.radial) + m.radial * m.radial

noncomputable def NavierStokes.MeanIncrementBounds.radialAngular {D : Type} (b m : Triple D) : Field D

Radial angular, given by (2 : ℝ) • (b.angular * m.angular) + m.angular * m.angular.

Equations

• NavierStokes.MeanIncrementBounds.radialAngular b m = 2 • (b.angular * m.angular) + m.angular * m.angular

noncomputable def NavierStokes.MeanIncrementBounds.thetaResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (b m : Triple D) (W : Fin 3 → Fin 3 → Field D) (T : Field D) : Field D

Theta residual, constructed using o.time.

Equations

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

noncomputable def NavierStokes.MeanIncrementBounds.axialResidual {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (b m : Triple D) (W : Fin 3 → Fin 3 → Field D) (p T : Field D) : Field D

Axial residual, constructed using o.time.

Equations

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

noncomputable def NavierStokes.MeanIncrementBounds.gr {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (b m : Triple D) (W : Fin 3 → Fin 3 → Field D) : Field D

Gr as an element of Field D.

Equations

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

noncomputable def NavierStokes.MeanIncrementBounds.deltaThetaRadial {D : Type} (b m h : Triple D) : Field D

Delta theta radial, given by b.radial * h.angular + h.radial * b.angular + m.radial * h.angular + h.radial * m.angular + h.radial * h.angular.

Equations

• NavierStokes.MeanIncrementBounds.deltaThetaRadial b m h = b.radial * h.angular + h.radial * b.angular + m.radial * h.angular + h.radial * m.angular + h.radial * h.angular

noncomputable def NavierStokes.MeanIncrementBounds.deltaThetaAxial {D : Type} (b m h : Triple D) : Field D

Delta theta axial, given by `b.axial * h.angular + b.angular * h.axial + m.axial * h.angular

• h.axial * m.angular + h.axial * h.angular`.

Equations

• NavierStokes.MeanIncrementBounds.deltaThetaAxial b m h = b.axial * h.angular + b.angular * h.axial + m.axial * h.angular + h.axial * m.angular + h.axial * h.angular

noncomputable def NavierStokes.MeanIncrementBounds.deltaAxialRadial {D : Type} (b m h : Triple D) : Field D

Delta axial radial, given by b.radial * h.axial + h.radial * b.axial + m.radial * h.axial + h.radial * m.axial + h.radial * h.axial.

Equations

• NavierStokes.MeanIncrementBounds.deltaAxialRadial b m h = b.radial * h.axial + h.radial * b.axial + m.radial * h.axial + h.radial * m.axial + h.radial * h.axial

noncomputable def NavierStokes.MeanIncrementBounds.deltaAxialAxial {D : Type} (b m h : Triple D) : Field D

Delta axial axial, given by (2 : ℝ) • (b.axial * h.axial) + (2 : ℝ) • (m.axial * h.axial) + h.axial * h.axial.

Equations

• NavierStokes.MeanIncrementBounds.deltaAxialAxial b m h = 2 • (b.axial * h.axial) + 2 • (m.axial * h.axial) + h.axial * h.axial

noncomputable def NavierStokes.MeanIncrementBounds.deltaRadialRadial {D : Type} (b m h : Triple D) : Field D

Delta radial radial, given by (2 : ℝ) • (b.radial * h.radial) + (2 : ℝ) • (m.radial * h.radial) + h.radial * h.radial.

Equations

• NavierStokes.MeanIncrementBounds.deltaRadialRadial b m h = 2 • (b.radial * h.radial) + 2 • (m.radial * h.radial) + h.radial * h.radial

noncomputable def NavierStokes.MeanIncrementBounds.radialAngularRemainder {D : Type} (m h : Triple D) : Field D

Radial angular remainder, given by (2 : ℝ) • (m.angular * h.angular) + h.angular * h.angular.

Equations

• NavierStokes.MeanIncrementBounds.radialAngularRemainder m h = 2 • (m.angular * h.angular) + h.angular * h.angular

noncomputable def NavierStokes.MeanIncrementBounds.leadingRadial {D : Type} (o : Operators D) (b h : Triple D) : Field D

Leading radial, given by o.invRadius * ((2 : ℝ) • (b.angular * h.angular)).

Equations

• NavierStokes.MeanIncrementBounds.leadingRadial o b h = o.invRadius * 2 • (b.angular * h.angular)

noncomputable def NavierStokes.MeanIncrementBounds.radialRemainder {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (b m h : Triple D) : Field D

Radial remainder as an element of Field D.

Equations

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

noncomputable def NavierStokes.MeanIncrementBounds.thetaRemainder {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (b m h : Triple D) : Field D

Theta remainder, given by o.slowTime h.angular + o.radialDiv 2 (deltaThetaRadial b m h) + o.dz (deltaThetaAxial b m h) - o.viscosity 1 h.angular.

Equations

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

noncomputable def NavierStokes.MeanIncrementBounds.axialRemainder {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (o : Operators D) (b m h : Triple D) (δp : Field D) : Field D

Axial remainder, given by o.slowTime h.axial + o.radialDiv 1 (deltaAxialRadial b m h) + o.dz (deltaAxialAxial b m h + δp) - o.viscosity 0 h.axial.

Equations

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

structure NavierStokes.MeanIncrementBounds.BaseBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (b : Triple D) : Prop

Base bounds data, collecting radial, angular, axial.

• radial : WeightedClasses.UnweightedClass s 1 b.radial
• angular : WeightedClasses.UnweightedClass s 0 b.angular
• axial : WeightedClasses.UnweightedClass s 0 b.axial

structure NavierStokes.MeanIncrementBounds.CumulativeBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (m : Triple D) : Prop

Cumulative bounds data, collecting radial, angular, axial.

• radial : WeightedClasses.MeanClass s (19 / 10) m.radial
• angular : WeightedClasses.MeanClass s (9 / 10) m.angular
• axial : WeightedClasses.MeanClass s (9 / 10) m.axial

structure NavierStokes.MeanIncrementBounds.IncrementBounds {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (H : ℝ) (h : Triple D) : Prop

Increment bounds data, collecting radial, angular, axial.

• radial : WeightedClasses.MeanClass s (H + 1) h.radial
• angular : WeightedClasses.MeanClass s H h.angular
• axial : WeightedClasses.MeanClass s H h.axial

theorem NavierStokes.MeanIncrementBounds.deltaThetaRadial_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 1) (deltaThetaRadial b m h)

theorem NavierStokes.MeanIncrementBounds.deltaThetaAxial_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s H (deltaThetaAxial b m h)

theorem NavierStokes.MeanIncrementBounds.deltaAxialRadial_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 1) (deltaAxialRadial b m h)

theorem NavierStokes.MeanIncrementBounds.deltaAxialAxial_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s H (deltaAxialAxial b m h)

theorem NavierStokes.MeanIncrementBounds.deltaRadialRadial_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 2) (deltaRadialRadial b m h)

theorem NavierStokes.MeanIncrementBounds.radialAngularRemainder_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {m h : Triple D} (ho : OperatorBounds s o κ) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 9 / 10) (radialAngularRemainder m h)

theorem NavierStokes.MeanIncrementBounds.leadingRadial_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hh : IncrementBounds s H h) : WeightedClasses.MeanClass s H (leadingRadial o b h)

theorem NavierStokes.MeanIncrementBounds.radialRemainder_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 9 / 10 - 2 * κ) (radialRemainder o b m h)

Every non-leading term of the actual radial pressure-source change has the stronger defect exponent. This includes fast time on the radial stream.

theorem NavierStokes.MeanIncrementBounds.thetaRemainder_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : WeightedClasses.MeanClass s (H + 1 - 2 * κ) (thetaRemainder o b m h)

theorem NavierStokes.MeanIncrementBounds.axialRemainder_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) {δp : Field D} (hp : WeightedClasses.MeanClass s H δp) : WeightedClasses.MeanClass s (H + 1 - 2 * κ) (axialRemainder o b m h δp)

structure NavierStokes.MeanIncrementBounds.SmoothTriple {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : Set D) (b : Triple D) : Prop

Smooth triple data, collecting radial, angular, axial.

• radial : SmoothOn U b.radial
• angular : SmoothOn U b.angular
• axial : SmoothOn U b.axial

theorem NavierStokes.MeanIncrementBounds.BaseBounds.smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {b : Triple D} (h : BaseBounds s b) : SmoothTriple s.domain b

theorem NavierStokes.MeanIncrementBounds.CumulativeBounds.smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {b : Triple D} (h : CumulativeBounds s b) : SmoothTriple s.domain b

theorem NavierStokes.MeanIncrementBounds.IncrementBounds.smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {H : ℝ} {b : Triple D} (h : IncrementBounds s H b) : SmoothTriple s.domain b

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.thetaRadial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) : SmoothOn U (MeanIncrementBounds.thetaRadial b m)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.thetaAxial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) : SmoothOn U (MeanIncrementBounds.thetaAxial b m)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.axialRadial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) : SmoothOn U (MeanIncrementBounds.axialRadial b m)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.axialAxial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) : SmoothOn U (MeanIncrementBounds.axialAxial b m)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.radialRadial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) : SmoothOn U (MeanIncrementBounds.radialRadial b m)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.deltaThetaRadial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) : SmoothOn U (MeanIncrementBounds.deltaThetaRadial b m h)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.deltaThetaAxial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) : SmoothOn U (MeanIncrementBounds.deltaThetaAxial b m h)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.deltaAxialRadial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) : SmoothOn U (MeanIncrementBounds.deltaAxialRadial b m h)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.deltaAxialAxial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) : SmoothOn U (MeanIncrementBounds.deltaAxialAxial b m h)

theorem NavierStokes.MeanIncrementBounds.SmoothTriple.deltaRadialRadial {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) : SmoothOn U (MeanIncrementBounds.deltaRadialRadial b m h)

theorem NavierStokes.MeanIncrementBounds.thetaRadial_updated {D : Type} (b m h : Triple D) : thetaRadial b (updated m h) = thetaRadial b m + deltaThetaRadial b m h

theorem NavierStokes.MeanIncrementBounds.thetaAxial_updated {D : Type} (b m h : Triple D) : thetaAxial b (updated m h) = thetaAxial b m + deltaThetaAxial b m h

theorem NavierStokes.MeanIncrementBounds.axialRadial_updated {D : Type} (b m h : Triple D) : axialRadial b (updated m h) = axialRadial b m + deltaAxialRadial b m h

theorem NavierStokes.MeanIncrementBounds.axialAxial_updated {D : Type} (b m h : Triple D) : axialAxial b (updated m h) = axialAxial b m + deltaAxialAxial b m h

theorem NavierStokes.MeanIncrementBounds.radialRadial_updated {D : Type} (b m h : Triple D) : radialRadial b (updated m h) = radialRadial b m + deltaRadialRadial b m h

theorem NavierStokes.MeanIncrementBounds.radialAngular_updated {D : Type} (b m h : Triple D) : radialAngular b (updated m h) = radialAngular b m + 2 • (b.angular * h.angular) + radialAngularRemainder m h

theorem NavierStokes.MeanIncrementBounds.thetaResidual_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) (ha : ContDiffOn ℝ (↑⊤) o.radialProfile U) {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn U (W i j)) (T : Field D) : Agree U (thetaResidual o b (updated m h) W T - thetaResidual o b m W T) (o.fastTime h.angular + thetaRemainder o b m h)

theorem NavierStokes.MeanIncrementBounds.axialResidual_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) (ha : ContDiffOn ℝ (↑⊤) o.radialProfile U) {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn U (W i j)) (p δp T : Field D) (hp : SmoothOn U p) (hδp : SmoothOn U δp) : Agree U (axialResidual o b (updated m h) W (p + δp) T - axialResidual o b m W p T) (o.fastTime h.axial + axialRemainder o b m h δp)

theorem NavierStokes.MeanIncrementBounds.gr_change {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (o : Operators D) (ha : ContDiffOn ℝ (↑⊤) o.radialProfile U) {b m h : Triple D} (hb : SmoothTriple U b) (hm : SmoothTriple U m) (hh : SmoothTriple U h) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn U (W i j)) : Agree U (gr o b (updated m h) W - gr o b m W) (leadingRadial o b h + radialRemainder o b m h)

theorem NavierStokes.MeanIncrementBounds.cumulative_updated {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {H : ℝ} {m h : Triple D} (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) : CumulativeBounds s (updated m h)

theorem NavierStokes.MeanIncrementBounds.thetaResidual_change_sub_fast_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn s.domain (W i j)) (T : Field D) : WeightedClasses.MeanClass s (H + 1 - 2 * κ) (thetaResidual o b (updated m h) W T - thetaResidual o b m W T - o.fastTime h.angular)

theorem NavierStokes.MeanIncrementBounds.axialResidual_change_sub_fast_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn s.domain (W i j)) (p δp T : Field D) (hp : SmoothOn s.domain p) (hδp : WeightedClasses.MeanClass s H δp) : WeightedClasses.MeanClass s (H + 1 - 2 * κ) (axialResidual o b (updated m h) W (p + δp) T - axialResidual o b m W p T - o.fastTime h.axial)

theorem NavierStokes.MeanIncrementBounds.gr_change_sub_leading_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn s.domain (W i j)) : WeightedClasses.MeanClass s (H + 9 / 10 - 2 * κ) (gr o b (updated m h) W - gr o b m W - leadingRadial o b h)

The actual radial source change retains the leading centrifugal term.

theorem NavierStokes.MeanIncrementBounds.gr_change_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn s.domain (W i j)) (hκ : 2 * κ ≤ 9 / 10) : WeightedClasses.MeanClass s H (gr o b (updated m h) W - gr o b m W)

theorem NavierStokes.MeanIncrementBounds.thetaResidual_change_slow_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn s.domain (W i j)) (T : Field D) (hslow : ∀ (n : ℕ), ∀ x ∈ s.domain, (fderiv ℝ (h.angular n) x) o.vT = 0) : WeightedClasses.MeanClass s (H + 1 - 2 * κ) (thetaResidual o b (updated m h) W T - thetaResidual o b m W T)

theorem NavierStokes.MeanIncrementBounds.axialResidual_change_slow_mem {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {o : Operators D} {κ H : ℝ} {b m h : Triple D} (ho : OperatorBounds s o κ) (hb : BaseBounds s b) (hm : CumulativeBounds s m) (hh : IncrementBounds s H h) (hH : 9 / 10 ≤ H) (W : Fin 3 → Fin 3 → Field D) (hW : ∀ (i j : Fin 3), SmoothOn s.domain (W i j)) (p δp T : Field D) (hp : SmoothOn s.domain p) (hδp : WeightedClasses.MeanClass s H δp) (hslow : ∀ (n : ℕ), ∀ x ∈ s.domain, (fderiv ℝ (h.axial n) x) o.vT = 0) : WeightedClasses.MeanClass s (H + 1 - 2 * κ) (axialResidual o b (updated m h) W (p + δp) T - axialResidual o b m W p T)

theorem NavierStokes.MeanIncrementBounds.directional_zero_of_line_const {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} {x v : D} (hf : DifferentiableAt ℝ f x) (hline : ∀ (t : ℝ), f (x + t • v) = f x) : (fderiv ℝ f x) v = 0

Independence along an actual affine line removes its Fréchet derivative.

theorem NavierStokes.MeanIncrementBounds.directional_zero_of_factor {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (π : D →L[ℝ] P) {f : P → ℝ} {x v : D} (hf : DifferentiableAt ℝ f (π x)) (hv : π v = 0) : (fderiv ℝ (fun (y : D) => f (π y)) x) v = 0

A field depending only on the slow projection has no fast derivative.

theorem NavierStokes.MeanIncrementBounds.radialSupport_sub {P : Type} {a b : ℝ} {f g : ℝ × P → ℝ} (hf : RadialAlias.RadiallySupported a b f) (hg : RadialAlias.RadiallySupported a b g) : RadialAlias.RadiallySupported a b fun (x : ℝ × P) => f x - g x

theorem NavierStokes.MeanIncrementBounds.interior_cutoff_meanClass {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR l r : ℝ} (ha : 0 < a) (hal : a < l) (hrb : r < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (χ : ℝ → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hs : Function.support χ ⊆ Set.Icc l r) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) 0 fun (x : ℕ) (x_1 : ℝ × P) => χ x_1.1

An interior radial cutoff belongs to the same flat mean class. The constant comes from its actual jets and the positive weight on its support.

theorem NavierStokes.MeanIncrementBounds.rho_meanClass {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) 0 fun (x : ℕ) (x_1 : ℝ × P) => PressureStream.rho a b hab x_1.1

The density in (33) is the actual normalized bump, not an assumed flat multiplier.

theorem NavierStokes.MeanIncrementBounds.pressureMass_sub {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} {f g : PressureStream.Lift P → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) : (PressureStream.pressureMass fun (x : PressureStream.Lift P) => f x - g x) = fun (p : P) => PressureStream.pressureMass f p - PressureStream.pressureMass g p

theorem NavierStokes.MeanIncrementBounds.pressureSource_sub {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b : ℝ} (hab : a < b) {f g : PressureStream.Lift P → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) : (PressureStream.pressureSource a b hab fun (x : PressureStream.Lift P) => f x - g x) = fun (x : PressureStream.Lift P) => PressureStream.pressureSource a b hab f x - PressureStream.pressureSource a b hab g x

theorem NavierStokes.MeanIncrementBounds.compactIntegral_sub {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b M : ℝ} {v : P} {f g : ℝ × P → ℝ} (hf : Continuous f) (hg : Continuous g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) (χ : ℝ → ℝ) (z : ℝ × P) : TransportPrimitive.compactIntegral χ M v (fun (x : ℝ × P) => f x - g x) z = TransportPrimitive.compactIntegral χ M v f z - TransportPrimitive.compactIntegral χ M v g z

theorem NavierStokes.MeanIncrementBounds.physicalCompact_sub {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {f g : ℝ × P → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : P) : (RadialPullback.physicalCompact d a b M v fun (x : ℝ × P) => f x - g x) = fun (x : ℝ × P) => RadialPullback.physicalCompact d a b M v f x - RadialPullback.physicalCompact d a b M v g x

theorem NavierStokes.MeanIncrementBounds.meanPressure_sub {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {f g : PressureStream.Lift P → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hsf : RadialAlias.RadiallySupported a b f) (hsg : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : PressureStream.Plane) : (PressureStream.meanPressure d a b M hab v fun (x : PressureStream.Lift P) => f x - g x) = fun (x : PressureStream.Lift P) => PressureStream.meanPressure d a b M hab v f x - PressureStream.meanPressure d a b M hab v g x

Recomputing (33) after an update is exactly applying its linear integral operator to the actual radial source difference.

theorem NavierStokes.MeanIncrementBounds.meanClass_pressureSource {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) => PressureStream.pressureSource a b hab (f n)

theorem NavierStokes.MeanIncrementBounds.meanClass_meanPressure {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → PressureStream.Lift P → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) => PressureStream.meanPressure d a b (M n) hab (v n) (f n)

The actual normalized shifted pressure primitive preserves every fixed-jet mean class, uniformly over its radial and torus shifts.

theorem NavierStokes.MeanIncrementBounds.meanClass_meanPressure_change {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f g : ℕ → PressureStream.Lift P → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hsf : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hsg : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α (f - g)) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) (x : ℝ × P × PressureStream.Plane) => PressureStream.meanPressure d a b (M n) hab (v n) (f n) x - PressureStream.meanPressure d a b (M n) hab (v n) (g n) x

noncomputable def NavierStokes.MeanIncrementBounds.reconstructedPressure {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d a b : ℝ) (hab : a < b) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (o : Operators (PressureStream.Lift P)) (base mean : Triple (PressureStream.Lift P)) (W : Fin 3 → Fin 3 → Field (PressureStream.Lift P)) : Field (PressureStream.Lift P)

Reconstructed pressure, defined pointwise by PressureStream.meanPressure d a b (M n) hab (v n) (gr o base mean W n).

Equations

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

theorem NavierStokes.MeanIncrementBounds.reconstructedPressure_change_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {κ H : ℝ} {o : Operators (PressureStream.Lift P)} {base mean inc : Triple (PressureStream.Lift P)} (ho : OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) o κ) (hb : BaseBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) base) (hm : CumulativeBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) mean) (hh : IncrementBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H inc) (hH : 9 / 10 ≤ H) (hκ : 2 * κ ≤ 9 / 10) (W : Fin 3 → Fin 3 → Field (PressureStream.Lift P)) (hW : ∀ (i j : Fin 3), SmoothOn (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS).domain (W i j)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (gr o base (updated mean inc) W n)) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (gr o base mean W n)) (hsf : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (gr o base (updated mean inc) W n)) (hsg : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (gr o base mean W n)) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H (reconstructedPressure d a b hab M v o base (updated mean inc) W - reconstructedPressure d a b hab M v o base mean W)

Pressure is recomputed from the literal gr; its change class is a conclusion, obtained from the centrifugal term and the exact remainder.

theorem NavierStokes.MeanIncrementBounds.tangential_recomputedPressure_change_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {κ H : ℝ} {o : Operators (PressureStream.Lift P)} {base mean inc : Triple (PressureStream.Lift P)} (ho : OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) o κ) (hb : BaseBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) base) (hm : CumulativeBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) mean) (hh : IncrementBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H inc) (hH : 9 / 10 ≤ H) (hκ : 2 * κ ≤ 9 / 10) (W : Fin 3 → Fin 3 → Field (PressureStream.Lift P)) (hW : ∀ (i j : Fin 3), SmoothOn (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS).domain (W i j)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (gr o base (updated mean inc) W n)) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (gr o base mean W n)) (hsf : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (gr o base (updated mean inc) W n)) (hsg : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (gr o base mean W n)) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (Tθ Tz : Field (PressureStream.Lift P)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) (H + 1 - 2 * κ) (thetaResidual o base (updated mean inc) W Tθ - thetaResidual o base mean W Tθ - o.fastTime inc.angular) ∧ WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) (H + 1 - 2 * κ) (axialResidual o base (updated mean inc) W (reconstructedPressure d a b hab M v o base (updated mean inc) W) Tz - axialResidual o base mean W (reconstructedPressure d a b hab M v o base mean W) Tz - o.fastTime inc.axial)

Every tangential effect beyond the actual fast derivative has the claimed exponent, including the recomputed axial pressure contribution.

theorem NavierStokes.MeanIncrementBounds.tangential_recomputedPressure_slow_change_mem {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {κ H : ℝ} {o : Operators (PressureStream.Lift P)} {base mean inc : Triple (PressureStream.Lift P)} (ho : OperatorBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) o κ) (hb : BaseBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) base) (hm : CumulativeBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) mean) (hh : IncrementBounds (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) H inc) (hH : 9 / 10 ≤ H) (hκ : 2 * κ ≤ 9 / 10) (W : Fin 3 → Fin 3 → Field (PressureStream.Lift P)) (hW : ∀ (i j : Fin 3), SmoothOn (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS).domain (W i j)) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (gr o base (updated mean inc) W n)) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (gr o base mean W n)) (hsf : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (gr o base (updated mean inc) W n)) (hsg : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (gr o base mean W n)) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (Tθ Tz : Field (PressureStream.Lift P)) (hslowθ : ∀ (n : ℕ), ∀ x ∈ (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS).domain, (fderiv ℝ (inc.angular n) x) o.vT = 0) (hslowz : ∀ (n : ℕ), ∀ x ∈ (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS).domain, (fderiv ℝ (inc.axial n) x) o.vT = 0) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) (H + 1 - 2 * κ) (thetaResidual o base (updated mean inc) W Tθ - thetaResidual o base mean W Tθ) ∧ WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) (H + 1 - 2 * κ) (axialResidual o base (updated mean inc) W (reconstructedPressure d a b hab M v o base (updated mean inc) W) Tz - axialResidual o base mean W (reconstructedPressure d a b hab M v o base mean W) Tz)

In the slow rank update the fast derivatives vanish, so the estimates hold directly for the full changes of the tangential residuals.

noncomputable def NavierStokes.MeanIncrementBounds.physicalOperators : Operators ProblemStatement.SpaceTime

The physical-coordinate instance identifies the chart expressions above with the already formalized equation (32). The slow time direction is -∂t because the chart's slow time term has a minus sign.

Equations

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

noncomputable def NavierStokes.MeanIncrementBounds.physicalField (f : MeanResidual.Scalar) : Field ProblemStatement.SpaceTime

Physical field, defined pointwise by f.

Equations

• NavierStokes.MeanIncrementBounds.physicalField f x✝ = f

noncomputable def NavierStokes.MeanIncrementBounds.physicalTriple (b : MeanResidual.Components) : Triple ProblemStatement.SpaceTime

Physical triple, given by ⟨physicalField (b 0), physicalField (b 1), physicalField (b 2)⟩.

Equations

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

noncomputable def NavierStokes.MeanIncrementBounds.physicalCovariance (w : MeanResidual.Components) : Fin 3 → Fin 3 → Field ProblemStatement.SpaceTime

Physical covariance, defined pointwise by physicalField (MeanResidual.covariance w i j).

Equations

• NavierStokes.MeanIncrementBounds.physicalCovariance w i j = NavierStokes.MeanIncrementBounds.physicalField (NavierStokes.MeanResidual.covariance w i j)

theorem NavierStokes.MeanIncrementBounds.physical_dr (f : Field ProblemStatement.SpaceTime) : physicalOperators.dr f = fun (n : ℕ) => MeanResidual.dr (f n)

theorem NavierStokes.MeanIncrementBounds.physical_dz (f : Field ProblemStatement.SpaceTime) : physicalOperators.dz f = fun (n : ℕ) => MeanResidual.dz (f n)

theorem NavierStokes.MeanIncrementBounds.physical_time (f : Field ProblemStatement.SpaceTime) : physicalOperators.time f = fun (n : ℕ) => MeanResidual.dt (f n)

theorem NavierStokes.MeanIncrementBounds.physical_radialDiv (c : ℝ) (f : Field ProblemStatement.SpaceTime) : physicalOperators.radialDiv c f = fun (n : ℕ) => MeanResidual.radialDivergence c (f n)

theorem NavierStokes.MeanIncrementBounds.physical_viscosity (c : ℝ) (f : Field ProblemStatement.SpaceTime) (n : ℕ) (q : ProblemStatement.SpaceTime) : physicalOperators.viscosity c f n q = MeanResidual.meanLaplacian (f n) q - c * (f n q / MeanResidual.radius q ^ 2)

theorem NavierStokes.MeanIncrementBounds.thetaResidual_eq_MeanResidual (b m w : MeanResidual.Components) (T : MeanResidual.Scalar) (n : ℕ) (q : ProblemStatement.SpaceTime) : thetaResidual physicalOperators (physicalTriple b) (physicalTriple m) (physicalCovariance w) (physicalField T) n q = MeanResidual.Etheta b m w T q

theorem NavierStokes.MeanIncrementBounds.axialResidual_eq_MeanResidual (b m w : MeanResidual.Components) (p T : MeanResidual.Scalar) (n : ℕ) (q : ProblemStatement.SpaceTime) : axialResidual physicalOperators (physicalTriple b) (physicalTriple m) (physicalCovariance w) (physicalField p) (physicalField T) n q = MeanResidual.Ez b m w p T q

theorem NavierStokes.MeanIncrementBounds.gr_eq_MeanResidual (b m w : MeanResidual.Components) (n : ℕ) (q : ProblemStatement.SpaceTime) : gr physicalOperators (physicalTriple b) (physicalTriple m) (physicalCovariance w) n q = MeanResidual.gr b m w q