Weighted classes of the actual base stress

The flat weight is transported exactly by the physical chart. Only powers of the reciprocal edge distance are enlarged. All derivatives are actual Fréchet derivatives, and every estimate is uniform over the dyadic bands.

@[reducible, inline]

abbrev NavierStokes.BaseStressClasses.Point : Type

Point: an abbreviation for BaseContextAssembly.Point.

Equations

• NavierStokes.BaseStressClasses.Point = NavierStokes.BaseContextAssembly.Point

@[reducible, inline]

abbrev NavierStokes.BaseStressClasses.Chart : Type

Chart: an abbreviation for SlowBorelBase.Chart.

Equations

• NavierStokes.BaseStressClasses.Chart = NavierStokes.SlowBorelBase.Chart

@[reducible, inline]

abbrev NavierStokes.BaseStressClasses.Inner : Type

Inner: an abbreviation for SlowBorelBase.Inner.

Equations

• NavierStokes.BaseStressClasses.Inner = NavierStokes.SlowBorelBase.Inner

theorem NavierStokes.BaseStressClasses.majorant_prefix {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (w : ℕ → D → ℝ) (α : ℝ) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (a : ℕ → ℕ → D → ℝ) (ha : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, a j n x ≤ WeightedClasses.majorant s w α C p n x) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ∀ j ≤ m, a j n x ≤ WeightedClasses.majorant s w α C p n x

Independent estimates for each derivative order give a single estimate for every fixed finite prefix. The polynomial degree may depend on the prefix, but never on the band or evaluation point.

theorem NavierStokes.BaseStressClasses.class_comp_of_outer_jets {D : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → E → V} {g : ℕ → D → E} {U : Set E} (hU : IsOpen U) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) U) (hg : WeightedClasses.UnweightedClass s 0 g) (hmap : ∀ (n : ℕ), Set.MapsTo (g n) s.domain U) (hw : ∀ (n : ℕ), ∀ x ∈ s.domain, 0 ≤ w n x) (hb : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), ∀ x ∈ s.domain, ‖iteratedFDeriv ℝ j (f n) (g n x)‖ ≤ WeightedClasses.majorant s w α C p n x) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n (g n x)

Weighted outer jets and a genuinely controlled inner map imply the class of the composite. In particular, no derivative estimate for the composite itself is assumed.

theorem NavierStokes.BaseStressClasses.scaled_jet_from_blown {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Chart → V} (hf : ContDiffOn ℝ (↑⊤) f BaseChartJets.sumRegion) {Q rho M : ℝ} {w : Inner} (hQ : 0 < Q) (hrho : 0 < rho) (hw : 0 < w.1) (hM : 1 ≤ M) (hi : 1 / rho ≤ M) (j : ℕ) : ‖iteratedFDeriv ℝ j (f ∘ ⇑(SlowBorelBase.scaleMap Q)) (rho, w)‖ ≤ ‖SlowBorelBase.blownJet j f (Q * rho, w)‖ * M ^ j

Banach-valued recentering of actual blown jets. The loss involves the bounded normalized scale rho, never the inverse dyadic scale.

noncomputable def NavierStokes.BaseStressClasses.coordinates {F : OutgoingProfile.Profile} (x : Point) : Chart

The exact normalized coordinates in the mean-variable order.

Equations

• NavierStokes.BaseStressClasses.coordinates x = NavierStokes.BaseChartJets.normalizedCoordinates F.data.h (NavierStokes.BaseContextAssembly.slowCoordinates x)

theorem NavierStokes.BaseStressClasses.coordinates_unweighted {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : WeightedClasses.UnweightedClass (BaseContextAssembly.nativeStrip W U) 0 fun (x : ℕ) => coordinates

theorem NavierStokes.BaseStressClasses.native_edgeDistance_le {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip W U).domain) : (BaseContextAssembly.nativeStrip W U).delta x ≤ FinalSlowBase.edgeDistance W (coordinates x).2

The source edge distance is the capped minimum of twice the two radial log distances. Thus it is at least the native strip distance.

theorem NavierStokes.BaseStressClasses.inverse_edgeDistance_le_growth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (n : ℕ) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip W U).domain) : (FinalSlowBase.edgeDistance W (coordinates x).2)⁻¹ ≤ (BaseContextAssembly.nativeStrip W U).growth n x

theorem NavierStokes.BaseStressClasses.coordinates_range {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) {x : Point} (hx : x ∈ (BaseContextAssembly.nativeStrip W U).domain) : (coordinates x).1 ∈ Set.Ioo (U.qlo / 2) (BaseContextAssembly.geometryUpper U)

theorem NavierStokes.BaseStressClasses.coordinate_power_unweighted {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) (a : ℝ) : WeightedClasses.UnweightedClass (BaseContextAssembly.nativeStrip W U) 0 fun (x : ℕ) (x_1 : BaseContextAssembly.Point) => (coordinates x_1).1 ^ a

Every fixed real power of the normalized positive scale has genuine uniform jets on the moving strip, including as physical time tends to zero.

noncomputable def NavierStokes.BaseStressClasses.correction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (y : Chart) : Inner

The literal positive-order part of the normalized tensor.

Equations

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

theorem NavierStokes.BaseStressClasses.correction_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (correction H v upper B) BaseChartJets.sumRegion

theorem NavierStokes.BaseStressClasses.correction_weighted_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) : ∃ (D : ℝ), 0 < D ∧ ∃ (N : ℕ), ∀ (q : ℝ), 0 < q → ∀ w ∈ FinalSlowBase.annulus W, ‖SlowBorelBase.blownJet m (correction H v upper B) (q, w)‖ ≤ D * q ^ F.data.h * FinalSlowBase.weight W w * (FinalSlowBase.edgeDistance W w)⁻¹ ^ N

The weighted normalized remainder estimate holds at every positive physical scale. Above one its actual blown jets vanish by the cutoff germ.

theorem NavierStokes.BaseStressClasses.leading_composed_meanClass {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 0 fun (x : ℕ) (x_1 : BaseContextAssembly.Point) => BaseResidual.stressPair (FinalSlowBase.coefficients H v) 0 (coordinates x_1).2

The order-zero tensor, composed with the actual moving chart, keeps the exact edge weight. Its proof uses the checked profile-jet estimates.

theorem NavierStokes.BaseStressClasses.correction_composed_meanClass {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)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 fun (n : ℕ) (x : BaseContextAssembly.Point) => correction H v upper B ((SlowBorelBase.scaleMap (ChartScales.Q n)) (coordinates x))

The actual positive-order normalized tensor is one mean order smaller after the band rescaling, uniformly over all bands.

theorem NavierStokes.BaseStressClasses.epsilon_bandBound {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : WeightedClasses.BandBound (BaseContextAssembly.nativeStrip W U) 1 (ChartScales.epsilon F.data.h)

The band scalar is exactly the first power of the class parameter.

theorem NavierStokes.BaseStressClasses.raw_leading_meanClass {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 fun (n : ℕ) (x : BaseContextAssembly.Point) => (ChartScales.epsilon F.data.h n * (coordinates x).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2)) • FinalSlowBase.leadingStress v (coordinates x).2

Raw positive-radius formula for the literal leading stress, including the exact physical power of the normalized similarity scale.

theorem NavierStokes.BaseStressClasses.raw_higher_meanClass {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)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 2 fun (n : ℕ) (x : BaseContextAssembly.Point) => (ChartScales.epsilon F.data.h n * (coordinates x).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2)) • (FinalSlowBase.normalizedStress H v upper B ((SlowBorelBase.scaleMap (ChartScales.Q n)) (coordinates x)) - FinalSlowBase.leadingStress v (coordinates x).2)

Raw positive-radius formula for the higher stress remainder. The extra mean order follows from the actual weighted Borel estimate and the physical band factor, without a lower bound on the flat weight.

theorem NavierStokes.BaseStressClasses.raw_stress_meanClass {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 fun (n : ℕ) (x : BaseContextAssembly.Point) => (ChartScales.epsilon F.data.h n * (coordinates x).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2)) • FinalSlowBase.normalizedStress H v upper B ((SlowBorelBase.scaleMap (ChartScales.Q n)) (coordinates x))

The full raw stress has mean order one.

theorem NavierStokes.BaseStressClasses.leadingVirtualStress_meanClass {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 (BaseContextAssembly.leadingVirtualStress H v)

The leading term of the same actual base context belongs to M₁.

theorem NavierStokes.BaseStressClasses.virtualStress_meanClass {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 (BaseContextAssembly.virtualStress H v upper B)

Actual virtual stress, with the signed-radius extension fixed by the base context. On this native strip the radius is strictly positive.

theorem NavierStokes.BaseStressClasses.higherStress_meanClass {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)) : WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 2 fun (n : ℕ) (x : BaseContextAssembly.Point) => BaseContextAssembly.virtualStress H v upper B n x - BaseContextAssembly.leadingVirtualStress H v n x

The difference between the actual virtual tensor and its actual leading term belongs to M₂, with constants uniform over every band.

theorem NavierStokes.BaseStressClasses.virtualStress_components {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (upper : ℝ) (B : ℕ) (U : LocalSignedRequest.SlowRegion (2 * F.data.h)) : (WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 fun (n : ℕ) (x : BaseContextAssembly.Point) => (BaseContextAssembly.virtualStress H v upper B n x).1) ∧ WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 1 fun (n : ℕ) (x : BaseContextAssembly.Point) => (BaseContextAssembly.virtualStress H v upper B n x).2

The two physical tensor entries can be consumed separately by the correction step, retaining the same strip and class exponent.

theorem NavierStokes.BaseStressClasses.higherStress_components {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)) : (WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 2 fun (n : ℕ) (x : BaseContextAssembly.Point) => (BaseContextAssembly.virtualStress H v upper B n x).1 - (BaseContextAssembly.leadingVirtualStress H v n x).1) ∧ WeightedClasses.MeanClass (BaseContextAssembly.nativeStrip W U) 2 fun (n : ℕ) (x : BaseContextAssembly.Point) => (BaseContextAssembly.virtualStress H v upper B n x).2 - (BaseContextAssembly.leadingVirtualStress H v n x).2