A physical signed request on its moving radial shell

The profile coordinate is R / sqrt(q). Its pullback retains the same flat edge weight as the primary field. All slow hypotheses are local; in particular no positive or bounded extension of q to the entire plane is assumed.

Mean reconstruction on an open slow domain

Radial transport and torus integration preserve the slow parameter. The operators in this file are the actual operators from PressureStream and TemporalMeanUpdate, restricted to an open slow domain. Cutoffs are used only to prove local smoothness and equality of germs; none of their derivatives enters the uniform estimates.

noncomputable def NavierStokes.PhysicalMeanDomain.slowDomain {S : Type} (U : Set S) : Set (PressureStream.Lift S)

All radii and torus variables, with only the slow parameter restricted.

Equations

• NavierStokes.PhysicalMeanDomain.slowDomain U = {p : NavierStokes.PressureStream.Lift S | p.2.1 ∈ U}

theorem NavierStokes.PhysicalMeanDomain.slowDomain_open {S : Type} [NormedAddCommGroup S] {U : Set S} (hU : IsOpen U) : IsOpen (slowDomain U)

noncomputable def NavierStokes.PhysicalMeanDomain.stripDomain {S : Type} (a b : ℝ) (U : Set S) : Set (PressureStream.Lift S)

Strip domain, given by {p | p.1 ∈ Ioo a b ∧ p.2.1 ∈ U}.

Equations

• NavierStokes.PhysicalMeanDomain.stripDomain a b U = {p : NavierStokes.PressureStream.Lift S | p.1 ∈ Set.Ioo a b ∧ p.2.1 ∈ U}

theorem NavierStokes.PhysicalMeanDomain.stripDomain_open {S : Type} [NormedAddCommGroup S] (a b : ℝ) {U : Set S} (hU : IsOpen U) : IsOpen (stripDomain a b U)

noncomputable def NavierStokes.PhysicalMeanDomain.localStripData {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) : WeightedClasses.StripData (PressureStream.Lift S)

Restriction changes only the domain, leaving all weights and band scales.

Equations

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

theorem NavierStokes.PhysicalMeanDomain.localStrip_majorant_eq {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) (α C : ℝ) (k n : ℕ) (p : PressureStream.Lift S) (hp : p.1 ∈ Set.Ioo a b) : WeightedClasses.majorant (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) (fun (x : ℕ) (x_1 : PressureStream.Lift S) => (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU).zeta x_1) α C k n p = C * ε n ^ α * L n ^ k * WeightedRadialPrimitive.logWeight cL cR a b k p.1

noncomputable def NavierStokes.PhysicalMeanDomain.SupportedOn {S V : Type} [NormedAddCommGroup V] (a b : ℝ) (U : Set S) (f : PressureStream.Lift S → V) : Prop

Radial support is required only at slow parameters where the source is used.

Equations

• NavierStokes.PhysicalMeanDomain.SupportedOn a b U f = ∀ (p : NavierStokes.PressureStream.Lift S), p.2.1 ∈ U → f p ≠ 0 → p.1 ∈ Set.Icc a b

noncomputable def NavierStokes.PhysicalMeanDomain.PeriodicOn {S : Type} (U : Set S) (f : PressureStream.Lift S → ℝ) : Prop

Periodic on, given by ∀ r s, s ∈ U → FourierAlias.TorusPeriodic (fun Y => f (r, (s, Y))).

Equations

• NavierStokes.PhysicalMeanDomain.PeriodicOn U f = ∀ (r : ℝ), ∀ s ∈ U, NavierStokes.FourierAlias.TorusPeriodic fun (Y : NavierStokes.TorusInverse.Plane) => f (r, s, Y)

noncomputable def NavierStokes.PhysicalMeanDomain.FiberGerm {S V : Type} [NormedAddCommGroup S] (s : S) (f g : PressureStream.Lift S → V) : Prop

The germ of a source on one entire slow fiber, including a slow neighborhood.

Equations

• NavierStokes.PhysicalMeanDomain.FiberGerm s f g = ∀ᶠ (t : S) in nhds s, ∀ (r : ℝ) (Y : NavierStokes.PressureStream.Plane), f (r, t, Y) = g (r, t, Y)

theorem NavierStokes.PhysicalMeanDomain.FiberGerm.eventuallyEq {S V : Type} [NormedAddCommGroup S] {s : S} {f g : PressureStream.Lift S → V} (h : FiberGerm s f g) (r : ℝ) (Y : PressureStream.Plane) : f =ᶠ[nhds (r, s, Y)] g

theorem NavierStokes.PhysicalMeanDomain.FiberGerm.jet_eq {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : S} {f g : PressureStream.Lift S → V} (h : FiberGerm s f g) (j : ℕ) (r : ℝ) (Y : PressureStream.Plane) : iteratedFDeriv ℝ j f (r, s, Y) = iteratedFDeriv ℝ j g (r, s, Y)

noncomputable def NavierStokes.PhysicalMeanDomain.localize {S V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c : S → ℝ) (f : PressureStream.Lift S → V) (p : PressureStream.Lift S) : V

An auxiliary localization, used only for germs.

Equations

• NavierStokes.PhysicalMeanDomain.localize c f p = c p.2.1 • f p

theorem NavierStokes.PhysicalMeanDomain.localize_smooth {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {U : Set S} (hU : IsOpen U) {c : S → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hcs : tsupport c ⊆ U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) : ContDiff ℝ (↑⊤) (localize c f)

theorem NavierStokes.PhysicalMeanDomain.localize_supported {S V : Type} [NormedAddCommGroup S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b : ℝ} {U : Set S} {c : S → ℝ} (hcs : tsupport c ⊆ U) {f : PressureStream.Lift S → V} (hs : SupportedOn a b U f) : RadialAlias.RadiallySupported a b (localize c f)

theorem NavierStokes.PhysicalMeanDomain.localize_periodic {S : Type} [NormedAddCommGroup S] {U : Set S} {c : S → ℝ} (hcs : tsupport c ⊆ U) {f : PressureStream.Lift S → ℝ} (hp : PeriodicOn U f) : PressureStream.TorusPeriodicLift (localize c f)

theorem NavierStokes.PhysicalMeanDomain.exists_fiber_localization {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ S] {U : Set S} (hU : IsOpen U) {s : S} (hs : s ∈ U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) : ∃ (c : S → ℝ), ContDiff ℝ (↑⊤) c ∧ tsupport c ⊆ U ∧ ContDiff ℝ (↑⊤) (localize c f) ∧ FiberGerm s (localize c f) f

noncomputable def NavierStokes.PhysicalMeanDomain.freezeSlow {S V : Type} (s : S) (f : PressureStream.Lift S → V) (p : PressureStream.Lift S) : V

Freezing the slow parameter never changes a radial transport integral on that fiber. It does not freeze any jet appearing in the integrand.

Equations

• NavierStokes.PhysicalMeanDomain.freezeSlow s f p = f (p.1, s, p.2.2)

theorem NavierStokes.PhysicalMeanDomain.freezeSlow_continuous {S V : Type} [NormedAddCommGroup S] [NormedAddCommGroup V] {f : PressureStream.Lift S → V} (hf : Continuous f) (s : S) : Continuous (freezeSlow s f)

theorem NavierStokes.PhysicalMeanDomain.freezeSlow_supported {S V : Type} [NormedAddCommGroup V] {a b : ℝ} {f : PressureStream.Lift S → V} (hs : RadialAlias.RadiallySupported a b f) (s : S) : RadialAlias.RadiallySupported a b (freezeSlow s f)

theorem NavierStokes.PhysicalMeanDomain.pastIntegral_freeze {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V) (p : PressureStream.Lift S) : TransportPrimitive.pastIntegral M (0, v) (freezeSlow p.2.1 f) p = TransportPrimitive.pastIntegral M (0, v) f p

theorem NavierStokes.PhysicalMeanDomain.totalIntegral_freeze {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V) (p : PressureStream.Lift S) : TransportPrimitive.totalIntegral M (0, v) (freezeSlow p.2.1 f) p = TransportPrimitive.totalIntegral M (0, v) f p

theorem NavierStokes.PhysicalMeanDomain.futureIntegral_freeze {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V) (p : PressureStream.Lift S) : TransportPrimitive.futureIntegral M (0, v) (freezeSlow p.2.1 f) p = TransportPrimitive.futureIntegral M (0, v) f p

Weighted estimates on one slow fiber

theorem NavierStokes.PhysicalMeanDomain.transport_past_left_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (k : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V), Continuous f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Ioo a b → (∀ X ∈ Set.Ioo a b, ∀ (Y : PressureStream.Plane), ‖f (X, z.2.1, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b k X) → WeightedRadialPrimitive.logPosition a z.1 ≤ WeightedRadialPrimitive.logLength a b / 2 → ‖TransportPrimitive.pastIntegral M (0, v) f z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b k z.1

theorem NavierStokes.PhysicalMeanDomain.transport_future_right_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (k : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V), Continuous f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Ioo a b → (∀ X ∈ Set.Ioo a b, ∀ (Y : PressureStream.Plane), ‖f (X, z.2.1, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b k X) → WeightedRadialPrimitive.logLength a b / 2 ≤ WeightedRadialPrimitive.logPosition a z.1 → ‖TransportPrimitive.futureIntegral M (0, v) f z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b k z.1

theorem NavierStokes.PhysicalMeanDomain.transport_mass_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (k : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V), Continuous f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Ioo a b → (∀ X ∈ Set.Ioo a b, ∀ (Y : PressureStream.Plane), ‖f (X, z.2.1, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b k X) → ‖TransportPrimitive.pastIntegral M (0, v) f z‖ ≤ K * A ∧ ‖TransportPrimitive.totalIntegral M (0, v) f z‖ ≤ K * A

theorem NavierStokes.PhysicalMeanDomain.transport_compact_finiteJets_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b c d cL cR : ℝ} (ha : 0 < a) (hac : a < c) (hcd : c < d) (hdb : d < b) (hcL : 0 < cL) (hcR : 0 < cR) (p m : ℕ) (χ : ℝ → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ X ≤ c, χ X = 0) (hright : ∀ (X : ℝ), d ≤ X → χ X = 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m, ∀ X ∈ Set.Ioo a b, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (X, s, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p X) → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Ioo a b → z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (TransportPrimitive.compactIntegral χ M (0, v) f) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b p z.1

theorem NavierStokes.PhysicalMeanDomain.canonical_transport_finiteJets_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m, ∀ X ∈ Set.Ioo a b, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (X, s, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p X) → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Ioo a b → z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (TransportPrimitive.compactIntegral (TransportPrimitive.interiorCutoff a b) M (0, v) f) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b p z.1

theorem NavierStokes.PhysicalMeanDomain.normalizeSource_finiteJets_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (cL cR : ℝ) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (g : PressureStream.Lift S → V), ContDiff ℝ (↑⊤) g → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m, ∀ R ∈ Set.Ioo a b, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j g (R, s, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p R) → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Ioo (a ^ d) (b ^ d) → z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (RadialPullback.normalizeSource d a g) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight (d ^ 2 * cL) (d ^ 2 * cR) (a ^ d) (b ^ d) p z.1

theorem NavierStokes.PhysicalMeanDomain.physicalCompact_finiteJets_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (g : PressureStream.Lift S → V), ContDiff ℝ (↑⊤) g → RadialAlias.RadiallySupported a b g → ∀ (A : ℝ), 0 ≤ A → ∀ (s : S), (∀ j ≤ m, ∀ R ∈ Set.Ioo a b, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j g (R, s, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p R) → ∀ (z : PressureStream.Lift S), z.1 ∈ Set.Ioo a b → z.2.1 = s → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (RadialPullback.physicalCompact d a b M (0, v) g) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR a b p z.1

The complete physical inverse preserves the original exponential weight and the same finite inverse-edge degree. All constants precede the arbitrary transport shift, source, amplitude, and evaluation point.

The actual operators preserve slow fibers and their germs

noncomputable def NavierStokes.PhysicalMeanDomain.FiberLocal {S V W : Type} (T : (PressureStream.Lift S → V) → PressureStream.Lift S → W) : Prop

Fiber local, given by ∀ (f g : PressureStream.Lift S → V) (s : S), (∀ r Y, f (r, (s, Y)) = g (r, (s, Y))) → ∀ r Y, T f (r, (s, Y)) = T g (r, (s, Y)).

Equations

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

theorem NavierStokes.PhysicalMeanDomain.FiberLocal.germ {S V : Type} [NormedAddCommGroup S] {W : Type} {T : (PressureStream.Lift S → V) → PressureStream.Lift S → W} (hT : FiberLocal T) {s : S} {f g : PressureStream.Lift S → V} (he : FiberGerm s f g) : FiberGerm s (T f) (T g)

theorem NavierStokes.PhysicalMeanDomain.physicalCompact_fiberLocal {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] (d a b M : ℝ) (v : PressureStream.Plane) : FiberLocal (RadialPullback.physicalCompact d a b M (0, v))

theorem NavierStokes.PhysicalMeanDomain.physicalAlias_fiberLocal {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] (d a b M : ℝ) (v : PressureStream.Plane) : FiberLocal (RadialPullback.physicalAlias d a b M (0, v))

theorem NavierStokes.PhysicalMeanDomain.weightedSource_fiberLocal {S : Type} : FiberLocal PressureStream.weightedSource

theorem NavierStokes.PhysicalMeanDomain.streamPotential_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : PressureStream.Plane) : FiberLocal (PressureStream.streamPotential d a b M (0, v))

theorem NavierStokes.PhysicalMeanDomain.liftedTorusAverage_fiberLocal {S : Type} : FiberLocal MeanMomentBounds.liftedTorusAverage

theorem NavierStokes.PhysicalMeanDomain.liftedPressureMass_fiberLocal {S : Type} : FiberLocal MeanMomentBounds.liftedPressureMass

theorem NavierStokes.PhysicalMeanDomain.pressureSource_fiberLocal {S : Type} (a b : ℝ) (hab : a < b) : FiberLocal (PressureStream.pressureSource a b hab)

theorem NavierStokes.PhysicalMeanDomain.meanPressure_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (hab : a < b) (v : PressureStream.Plane) : FiberLocal (PressureStream.meanPressure d a b M hab v)

theorem NavierStokes.PhysicalMeanDomain.centered_fiberLocal {S : Type} : FiberLocal TemporalMeanUpdate.centered

theorem NavierStokes.PhysicalMeanDomain.FiberLocal.contDiffOn_of_supported {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ S] {T : (PressureStream.Lift S → V) → PressureStream.Lift S → W} (hT : FiberLocal T) {a b : ℝ} (hTs : ∀ (f : ℝ × S × PressureStream.Plane → V), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → ContDiff ℝ (↑⊤) (T f)) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (T f) (slowDomain U)

A proved fiber-local operator transfers its global smoothness theorem to local input data. No global extension is an input to this theorem.

theorem NavierStokes.PhysicalMeanDomain.physicalCompact_contDiffOn {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (RadialPullback.physicalCompact d a b M (0, v) f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.physicalAlias_contDiffOn {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (RadialPullback.physicalAlias d a b M (0, v) f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.streamPotential_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (PressureStream.streamPotential d a b M (0, v) f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.meanPressure_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (PressureStream.meanPressure d a b M hab v f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.liftedPressureMass_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (MeanMomentBounds.liftedPressureMass f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.meanClass_physicalCompact {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [FiniteDimensional ℝ S] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (f : ℕ → PressureStream.Lift S → V) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => RadialPullback.physicalCompact d a b (M n) (0, v n) (f n)

theorem NavierStokes.PhysicalMeanDomain.iteratedFDeriv_affineAverage {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) (v : E) {a b : ℝ} (hab : a ≤ b) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (j : ℕ) (x : D) : iteratedFDeriv ℝ j (MeanMomentBounds.affineAverage L v a b f) x = ∫ (t : ℝ) in a..b, iteratedFDeriv ℝ j (fun (y : D) => f (L y + t • v)) x

Compact integration needs local domination only, not a bound on all parameters. This identity differentiates the literal affine average.

theorem NavierStokes.PhysicalMeanDomain.affineAverage_jet_bound {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) (v : E) {a b : ℝ} (hab : a ≤ b) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (j : ℕ) (x : D) (C : ℝ) (hC : ∀ t ∈ Set.Icc a b, ‖iteratedFDeriv ℝ j f (L x + t • v)‖ ≤ C) : ‖iteratedFDeriv ℝ j (MeanMomentBounds.affineAverage L v a b f) x‖ ≤ C * (b - a)

theorem NavierStokes.PhysicalMeanDomain.liftedTorusAverage_jet_bound {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (j : ℕ) (p : PressureStream.Lift S) (C : ℝ) (hb : ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (p.1, p.2.1, Y)‖ ≤ C) : ‖iteratedFDeriv ℝ j (MeanMomentBounds.liftedTorusAverage f) p‖ ≤ C

theorem NavierStokes.PhysicalMeanDomain.FiberLocal.contDiffOn {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ S] {T : (PressureStream.Lift S → V) → PressureStream.Lift S → W} (hT : FiberLocal T) (hTs : ∀ (f : PressureStream.Lift S → V), ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) (T f)) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) : ContDiffOn ℝ (↑⊤) (T f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.FiberLocal.contDiffOn_of_periodic {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {T : (PressureStream.Lift S → ℝ) → PressureStream.Lift S → ℝ} (hT : FiberLocal T) (hTs : ∀ (f : PressureStream.Lift S → ℝ), ContDiff ℝ (↑⊤) f → PressureStream.TorusPeriodicLift f → ContDiff ℝ (↑⊤) (T f)) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hp : PeriodicOn U f) : ContDiffOn ℝ (↑⊤) (T f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.FiberLocal.supportedOn {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type} [NormedAddCommGroup W] [FiniteDimensional ℝ S] {T : (PressureStream.Lift S → V) → PressureStream.Lift S → W} (hT : FiberLocal T) {a b : ℝ} (hTs : ∀ (f : ℝ × S × PressureStream.Plane → V), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → RadialAlias.RadiallySupported a b (T f)) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : SupportedOn a b U (T f)

theorem NavierStokes.PhysicalMeanDomain.liftedTorusAverage_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) : ContDiffOn ℝ (↑⊤) (MeanMomentBounds.liftedTorusAverage f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.liftedTorusAverage_supportedOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : SupportedOn a b U (MeanMomentBounds.liftedTorusAverage f)

theorem NavierStokes.PhysicalMeanDomain.centered_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) : ContDiffOn ℝ (↑⊤) (TemporalMeanUpdate.centered f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.centered_periodicOn {S : Type} {U : Set S} {f : PressureStream.Lift S → ℝ} (hp : PeriodicOn U f) : PeriodicOn U (TemporalMeanUpdate.centered f)

theorem NavierStokes.PhysicalMeanDomain.meanClass_liftedTorusAverage {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => MeanMomentBounds.liftedTorusAverage (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_centered {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => TemporalMeanUpdate.centered (f n)

theorem NavierStokes.PhysicalMeanDomain.jet_zero_outside {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ S] {a b : ℝ} {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → V} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) {p : PressureStream.Lift S} (hp : p.2.1 ∈ U) (hr : p.1 ∉ Set.Ioo a b) (j : ℕ) : iteratedFDeriv ℝ j f p = 0

noncomputable def NavierStokes.PhysicalMeanDomain.LocalBandJets {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] (U : Set S) (ε L : ℕ → ℝ) (α : ℝ) (f : ℕ → PressureStream.Lift S → V) : Prop

Uniform band jets on the valid slow domain, including all radial edges.

Equations

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

theorem NavierStokes.PhysicalMeanDomain.meanClass_localBandJets {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → V} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : LocalBandJets U ε L α f

theorem NavierStokes.PhysicalMeanDomain.memClass_restrict {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {w : ℕ → PressureStream.Lift S → ℝ} {f : ℕ → PressureStream.Lift S → V} (hf : WeightedClasses.MemClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε L hε hεone hL) w α f) : WeightedClasses.MemClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) w α f

theorem NavierStokes.PhysicalMeanDomain.liftedPressureMass_jet_bound {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (hab : a ≤ b) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (j : ℕ) (p : PressureStream.Lift S) (C : ℝ) (hb : ∀ R ∈ Set.Icc a b, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, p.2.1, Y)‖ ≤ C) : ‖iteratedFDeriv ℝ j (MeanMomentBounds.liftedPressureMass f) p‖ ≤ C * (b - a)

theorem NavierStokes.PhysicalMeanDomain.LocalBandJets.liftedPressureMass {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} (hab : a ≤ b) {U : Set S} (hU : IsOpen U) {ε L : ℕ → ℝ} {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hjets : LocalBandJets U ε L α f) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) : LocalBandJets U ε L α fun (n : ℕ) => MeanMomentBounds.liftedPressureMass (f n)

theorem NavierStokes.PhysicalMeanDomain.localBandJets_unweighted {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → V} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hjets : LocalBandJets U ε L α f) : WeightedClasses.UnweightedClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f

theorem NavierStokes.PhysicalMeanDomain.meanClass_pressureMass_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.UnweightedClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) (p : PressureStream.Lift S) => PressureStream.pressureMass (f n) p.2.1

theorem NavierStokes.PhysicalMeanDomain.meanClass_radialMultiply {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) (p : PressureStream.Lift S) => φ p.1 * f n p

theorem NavierStokes.PhysicalMeanDomain.pressureSource_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} (hab : a < b) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (PressureStream.pressureSource a b hab f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.pressureSource_supportedOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b : ℝ} (hab : a < b) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : SupportedOn a b U (PressureStream.pressureSource a b hab f)

theorem NavierStokes.PhysicalMeanDomain.meanClass_pressureSource {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => PressureStream.pressureSource a b hab (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_meanPressure {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => PressureStream.meanPressure d a b (M n) hab (v n) (f n)

noncomputable def NavierStokes.PhysicalMeanDomain.localSlowStripData {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (U : Set S) (hU : IsOpen U) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) : WeightedClasses.StripData S

Local slow strip data as an element of StripData S.

Equations

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

theorem NavierStokes.PhysicalMeanDomain.meanClass_pressureMass {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.UnweightedClass (localSlowStripData U hU ε L hε hεone hL) α fun (n : ℕ) => PressureStream.pressureMass (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_radialMoment_lift {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (k : ℕ) : WeightedClasses.UnweightedClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) (p : PressureStream.Lift S) => IntegratedMeanBalances.radialMoment k (PressureStream.torusAverage (f n)) p.2.1

theorem NavierStokes.PhysicalMeanDomain.meanClass_radialMoment {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (k : ℕ) : WeightedClasses.UnweightedClass (localSlowStripData U hU ε L hε hεone hL) α fun (n : ℕ) => IntegratedMeanBalances.radialMoment k (PressureStream.torusAverage (f n))

theorem NavierStokes.PhysicalMeanDomain.SupportedOn.sub {S : Type} {a b : ℝ} {U : Set S} {f g : PressureStream.Lift S → ℝ} (hf : SupportedOn a b U f) (hg : SupportedOn a b U g) : SupportedOn a b U fun (p : PressureStream.Lift S) => f p - g p

theorem NavierStokes.PhysicalMeanDomain.meanPressure_sub_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f g : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hg : ContDiffOn ℝ (↑⊤) g (slowDomain U)) (hsf : SupportedOn a b U f) (hsg : SupportedOn a b U g) {p : PressureStream.Lift S} (hp : p.2.1 ∈ U) : PressureStream.meanPressure d a b M hab v (fun (x : PressureStream.Lift S) => f x - g x) p = PressureStream.meanPressure d a b M hab v f p - PressureStream.meanPressure d a b M hab v g p

The local pressure is the same linear integral operator used globally.

theorem NavierStokes.PhysicalMeanDomain.meanClass_meanPressure_change {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f g : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hg : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (g n) (slowDomain U)) (hsf : ∀ (n : ℕ), SupportedOn a b U (f n)) (hsg : ∀ (n : ℕ), SupportedOn a b U (g n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α (f - g)) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) (p : PressureStream.Lift S) => PressureStream.meanPressure d a b (M n) hab (v n) (f n) p - PressureStream.meanPressure d a b (M n) hab (v n) (g n) p

Exact identification of the positive-time normalized rank domain

noncomputable def NavierStokes.PhysicalMeanDomain.normalizedSlowDomain (coord qlo qhi : ℝ) : Set PressureStream.Plane

Normalized slow domain, given by {s | 0 < s.1 ∧ SimilarityCoordinates.coordinateQ coord (s.1, s.2) ∈ Ioo qlo qhi}.

Equations

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

theorem NavierStokes.PhysicalMeanDomain.chartQ_eq_slow (coord : ℝ) (p : MeanRankUpdate.ChartPoint) : MeanRankUpdate.chartQ coord p = SimilarityCoordinates.coordinateQ coord (p.2.1.1, p.2.1.2)

theorem NavierStokes.PhysicalMeanDomain.normalizedSlowDomain_open {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (qlo qhi : ℝ) : IsOpen (normalizedSlowDomain coord qlo qhi)

theorem NavierStokes.PhysicalMeanDomain.normalizedDomain_eq (coord qlo qhi rlo rhi : ℝ) : MeanRankUpdate.normalizedDomain coord qlo qhi rlo rhi = stripDomain rlo rhi (normalizedSlowDomain coord qlo qhi)

theorem NavierStokes.PhysicalMeanDomain.normalizedStripData_eq (coord qlo qhi rlo rhi cL cR : ℝ) (hc : 0 < coord) (hc1 : coord < 1) (hrlo : 0 < rlo) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) : MeanRankUpdate.normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε L hε hεone hL = localStripData rlo rhi cL cR hrlo hcL hcR ε L hε hεone hL (normalizedSlowDomain coord qlo qhi) ⋯

theorem NavierStokes.PhysicalMeanDomain.temporalInverse_fiberLocal {S : Type} : FiberLocal TemporalMeanUpdate.temporalInverse

theorem NavierStokes.PhysicalMeanDomain.temporalInverse_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hp : PeriodicOn U f) : ContDiffOn ℝ (↑⊤) (TemporalMeanUpdate.temporalInverse f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.meanClass_temporalInverse {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hp : ∀ (n : ℕ), PeriodicOn U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => TemporalMeanUpdate.temporalInverse (f n)

theorem NavierStokes.PhysicalMeanDomain.desiredIncrement_fiberLocal {S : Type} (h : ℝ) (n : ℕ) : FiberLocal (TemporalMeanUpdate.desiredIncrement h n)

theorem NavierStokes.PhysicalMeanDomain.desiredIncrement_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hp : PeriodicOn U f) : ContDiffOn ℝ (↑⊤) (TemporalMeanUpdate.desiredIncrement h n f) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.desiredIncrement_supportedOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {a b : ℝ} {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : SupportedOn a b U (TemporalMeanUpdate.desiredIncrement h n f)

theorem NavierStokes.PhysicalMeanDomain.meanClass_desiredIncrement {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR h : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hp : ∀ (n : ℕ), PeriodicOn U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => TemporalMeanUpdate.desiredIncrement h n (f n)

theorem NavierStokes.PhysicalMeanDomain.dividedAlias_finiteJets_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (g : PressureStream.Lift S → ℝ), ContDiff ℝ (↑⊤) g → RadialAlias.RadiallySupported a b g → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), (∀ j ≤ m, ∀ (z : PressureStream.Lift S), z.2.1 = s → ‖iteratedFDeriv ℝ j (UniformFourierAlias.exactAlias (TransportPrimitive.interiorCutoff (a ^ d) (b ^ d)) M (0, v) (RadialPullback.normalizeSource d a g)) z‖ ≤ C) → ∀ j ≤ m, ∀ (z : PressureStream.Lift S), z.2.1 = s → ‖iteratedFDeriv ℝ j (PressureStream.divideRadius (RadialPullback.physicalAlias d a b M (0, v) g)) z‖ ≤ K * C

theorem NavierStokes.PhysicalMeanDomain.totalIntegral_jet_bound_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b M : ℝ} (hab : a ≤ b) (v : PressureStream.Plane) {f : PressureStream.Lift S → V} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (j : ℕ) (p : PressureStream.Lift S) (C : ℝ) (hb : ∀ R ∈ Set.Icc a b, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j f (R, p.2.1, Y)‖ ≤ C) : ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M (0, v) f) p‖ ≤ C * (b - a)

theorem NavierStokes.PhysicalMeanDomain.exactAlias_bounded_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b : ℝ} (hab : a ≤ b) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → V), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), (∀ i ≤ m, ∀ R ∈ Set.Icc a b, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ i f (R, s, Y)‖ ≤ C) → ∀ j ≤ m, ∀ (z : PressureStream.Lift S), z.2.1 = s → ‖iteratedFDeriv ℝ j (UniformFourierAlias.exactAlias χ M (0, v) f) z‖ ≤ K * C

A bounded source gives a bounded actual cutoff alias, with a constant independent of the transport shift and the slow fiber.

theorem NavierStokes.PhysicalMeanDomain.normalizeSource_bounded_fiber {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] {a d : ℝ} (ha : 0 < a) (hd : 0 < d) (lo hi : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : PressureStream.Lift S → V), ContDiff ℝ (↑⊤) f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), (∀ i ≤ m, ∀ (R : ℝ) (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ i f (R, s, Y)‖ ≤ C) → ∀ j ≤ m, ∀ R ∈ Set.Icc lo hi, ∀ (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ j (RadialPullback.normalizeSource d a f) (R, s, Y)‖ ≤ K * C

theorem NavierStokes.PhysicalMeanDomain.dividedAlias_bounded_fiber {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : PressureStream.Plane) (f : PressureStream.Lift S → ℝ), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → ∀ (C : ℝ), 0 ≤ C → ∀ (s : S), (∀ i ≤ m, ∀ (R : ℝ) (Y : PressureStream.Plane), ‖iteratedFDeriv ℝ i f (R, s, Y)‖ ≤ C) → ∀ j ≤ m, ∀ (z : PressureStream.Lift S), z.2.1 = s → ‖iteratedFDeriv ℝ j (PressureStream.divideRadius (RadialPullback.physicalAlias d a b M (0, v) f)) z‖ ≤ K * C

theorem NavierStokes.PhysicalMeanDomain.dividedAlias_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (v : PressureStream.Plane) : FiberLocal fun (f : PressureStream.Lift S → ℝ) => PressureStream.divideRadius (RadialPullback.physicalAlias d a b M (0, v) f)

theorem NavierStokes.PhysicalMeanDomain.dividedAlias_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (PressureStream.divideRadius (RadialPullback.physicalAlias d a b M (0, v) f)) (slowDomain U)

theorem NavierStokes.PhysicalMeanDomain.LocalBandJets.dividedAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {U : Set S} (hU : IsOpen U) {ε L : ℕ → ℝ} (hε : ∀ (n : ℕ), 0 < ε n) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hjets : LocalBandJets U ε L α f) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : LocalBandJets U ε L α fun (n : ℕ) => PressureStream.divideRadius (RadialPullback.physicalAlias d a b (M n) (0, v n) (f n))

theorem NavierStokes.PhysicalMeanDomain.localBandJets_meanClass_of_support {S V : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ S] {a b c e cL cR : ℝ} (ha : 0 < a) (hac : a < c) (heb : e < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → V} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn c e U (f n)) (hb : LocalBandJets U ε L α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f

theorem NavierStokes.PhysicalMeanDomain.meanClass_dividedAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => PressureStream.divideRadius (RadialPullback.physicalAlias d a b (M n) (0, v n) (f n))

The actual divided alias preserves the local mean class. No mean-zero condition or nonzero transport coefficient is needed for this basic bound.

theorem NavierStokes.PhysicalMeanDomain.meanClass_divideRadius {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => PressureStream.divideRadius (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_streamPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => PressureStream.streamPotential d a b (M n) (0, v n) (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_streamBeta {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : S × PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => PressureStream.streamBeta w (PressureStream.streamPotential d a b (M n) (0, v n) (f n))

theorem NavierStokes.PhysicalMeanDomain.streamGamma_eq_desired_sub_alias_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) {p : PressureStream.Lift S} (hp : p.2.1 ∈ U) : PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (PressureStream.streamPotential d a b M (0, v) f) p = f p - RadialPullback.physicalAlias d a b M (0, v) (PressureStream.weightedSource f) p / p.1

theorem NavierStokes.PhysicalMeanDomain.meanClass_streamGamma {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => PressureStream.streamGamma (PressureStream.physicalSpeed d (M n)) (0, v n) (PressureStream.streamPotential d a b (M n) (0, v n) (f n))

theorem NavierStokes.PhysicalMeanDomain.stream_divergence_zero_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) (w : S × PressureStream.Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hs : SupportedOn a b U f) {p : PressureStream.Lift S} (hp : p.2.1 ∈ U) (hr : p.1 ≠ 0) : PressureStream.graphDivergence (PressureStream.physicalSpeed d M) (0, v) w (PressureStream.streamBeta w (PressureStream.streamPotential d a b M (0, v) f)) (PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (PressureStream.streamPotential d a b M (0, v) f)) p = 0

theorem NavierStokes.PhysicalMeanDomain.desiredIncrement_zeroMean_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hper : PeriodicOn U f) (p : ℝ × S) (hp : p.2 ∈ U) : PressureStream.torusAverage (TemporalMeanUpdate.desiredIncrement h n f) p = 0

theorem NavierStokes.PhysicalMeanDomain.desiredIncrement_barMass_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hper : PeriodicOn U f) (w : ℝ → ℝ) (s : S) (hs : s ∈ U) : ∫ (r : ℝ), w r * PressureStream.torusAverage (TemporalMeanUpdate.desiredIncrement h n f) (r, s) = 0

theorem NavierStokes.PhysicalMeanDomain.desiredIncrement_fastDerivative_on {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n : ℕ) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (slowDomain U)) (hper : PeriodicOn U f) {p : PressureStream.Lift S} (hp : p.2.1 ∈ U) : TemporalMeanUpdate.fastDerivative h n (TemporalMeanUpdate.desiredIncrement h n f) p = -TemporalMeanUpdate.centered f p

theorem NavierStokes.PhysicalMeanDomain.meanClass_axialPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hp : ∀ (n : ℕ), PeriodicOn U (f n)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => TemporalMeanUpdate.axialPotential d a b (M n) (v n) h n (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_radialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hp : ∀ (n : ℕ), PeriodicOn U (f n)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : S × PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => TemporalMeanUpdate.radialUpdate d a b (M n) (v n) w h n (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_scaledRadialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hp : ∀ (n : ℕ), PeriodicOn U (f n)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : S × PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) (α + 1) fun (n : ℕ) => TemporalMeanUpdate.radialUpdate d a b (M n) (v n) (ε n • w) h n (f n)

theorem NavierStokes.PhysicalMeanDomain.meanClass_axialUpdate {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b d cL cR h : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 ≤ h) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (hscale : ∀ (n : ℕ), ChartScales.S n ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (slowDomain U)) (hp : ∀ (n : ℕ), PeriodicOn U (f n)) (hs : ∀ (n : ℕ), SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) : WeightedClasses.MeanClass (localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => TemporalMeanUpdate.axialUpdate d a b (M n) (v n) h n (f n)

@[reducible, inline]

abbrev NavierStokes.LocalSignedRequest.Plane : Type

Plane: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.LocalSignedRequest.Plane = NavierStokes.PressureStream.Plane

@[reducible, inline]

abbrev NavierStokes.LocalSignedRequest.Point : Type

Point: an abbreviation for PressureStream.Lift Plane.

Equations

• NavierStokes.LocalSignedRequest.Point = NavierStokes.PressureStream.Lift NavierStokes.LocalSignedRequest.Plane

noncomputable def NavierStokes.LocalSignedRequest.localPullbackStrip {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData D) (Φ : E → D) (U : Set E) (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) : WeightedClasses.StripData E

The exact pullback of the weights, with a local domain for the map.

Equations

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

noncomputable def NavierStokes.LocalSignedRequest.BoundedPositiveJets {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (Φ : E → D) (U : Set E) : Prop

Positive jets, rather than the value of an unbounded auxiliary coordinate, are what the composition estimate uses.

Equations

• NavierStokes.LocalSignedRequest.BoundedPositiveJets Φ U = ∀ (m : ℕ), ∃ (B : ℝ), 1 ≤ B ∧ ∀ (j : ℕ), 1 ≤ j → j ≤ m → ∀ x ∈ U, ‖iteratedFDeriv ℝ j Φ x‖ ≤ B

theorem NavierStokes.LocalSignedRequest.class_comp {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData D} {t : WeightedClasses.StripData E} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → F} (hf : WeightedClasses.MemClass s w α f) (Φ : E → D) (hΦ : ContDiffOn ℝ (↑⊤) Φ t.domain) (hmap : Set.MapsTo Φ t.domain s.domain) (hε : ∀ (n : ℕ), t.epsilon n = s.epsilon n) (hL : ∀ (n : ℕ), t.slow n = s.slow n) (hδ : ∀ x ∈ t.domain, t.delta x = s.delta (Φ x)) (hjets : BoundedPositiveJets Φ t.domain) : WeightedClasses.MemClass t (fun (n : ℕ) (x : E) => w n (Φ x)) α fun (n : ℕ) (x : E) => f n (Φ x)

theorem NavierStokes.LocalSignedRequest.class_localPullback {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → F} (hf : WeightedClasses.MemClass s w α f) (Φ : E → D) (U : Set E) (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (hjets : BoundedPositiveJets Φ (U ∩ Φ ⁻¹' s.domain)) : WeightedClasses.MemClass (localPullbackStrip s Φ U hU hΦ) (fun (n : ℕ) (x : E) => w n (Φ x)) α fun (n : ℕ) (x : E) => f n (Φ x)

structure NavierStokes.LocalSignedRequest.SlowRegion (coord : ℝ) : Type

A genuine open positive-time region with bounds on the actual normalized similarity coordinate. Its endpoints and constants are independent of bands.

• carrier : Set Plane

  Carrier of SlowRegion, of type Set Plane.

• isOpen : IsOpen self.carrier
• coord_pos : 0 < coord
• coord_lt_one : coord < 1
• qlo : ℝ

  Qlo of SlowRegion, of type ℝ.

• qhi : ℝ

  Qhi of SlowRegion, of type ℝ.

• qlo_pos : 0 < self.qlo
• time_pos (s : Plane) : s ∈ self.carrier → 0 < s.1
• q_mem (s : Plane) : s ∈ self.carrier → SimilarityCoordinates.coordinateQ coord s ∈ Set.Icc self.qlo self.qhi

noncomputable def NavierStokes.LocalSignedRequest.profileMap (coord : ℝ) (x : Point) : Point

Profile map, given by (x.1 / Real.sqrt (MeanRankUpdate.chartQ coord x), x.2).

Equations

• NavierStokes.LocalSignedRequest.profileMap coord x = (x.1 / √(NavierStokes.MeanRankUpdate.chartQ coord x), x.2)

noncomputable def NavierStokes.LocalSignedRequest.inverseProfileMap (coord : ℝ) (x : Point) : Point

Inverse profile map, given by (Real.sqrt (MeanRankUpdate.chartQ coord x) * x.1, x.2).

Equations

• NavierStokes.LocalSignedRequest.inverseProfileMap coord x = (√(NavierStokes.MeanRankUpdate.chartQ coord x) * x.1, x.2)

@[simp]

theorem NavierStokes.LocalSignedRequest.chartQ_profileMap (coord : ℝ) (x : Point) : MeanRankUpdate.chartQ coord (profileMap coord x) = MeanRankUpdate.chartQ coord x

@[simp]

theorem NavierStokes.LocalSignedRequest.chartQ_inverseProfileMap (coord : ℝ) (x : Point) : MeanRankUpdate.chartQ coord (inverseProfileMap coord x) = MeanRankUpdate.chartQ coord x

theorem NavierStokes.LocalSignedRequest.profileMap_inverse (coord : ℝ) (x : Point) (hq : 0 < MeanRankUpdate.chartQ coord x) : profileMap coord (inverseProfileMap coord x) = x

theorem NavierStokes.LocalSignedRequest.inverseProfileMap_profile (coord : ℝ) (x : Point) (hq : 0 < MeanRankUpdate.chartQ coord x) : inverseProfileMap coord (profileMap coord x) = x

theorem NavierStokes.LocalSignedRequest.profileMap_smooth {coord : ℝ} (U : SlowRegion coord) : ContDiffOn ℝ (↑⊤) (profileMap coord) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.LocalSignedRequest.inverseProfileMap_smooth {coord : ℝ} (U : SlowRegion coord) : ContDiffOn ℝ (↑⊤) (inverseProfileMap coord) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.LocalSignedRequest.SlowRegion.chartQ_pos {coord : ℝ} (U : SlowRegion coord) {x : Point} (hx : x.2.1 ∈ U.carrier) : 0 < MeanRankUpdate.chartQ coord x

noncomputable def NavierStokes.LocalSignedRequest.movingStripData {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) : WeightedClasses.StripData Point

Moving strip data, constructed using localPullbackStrip.

Equations

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

theorem NavierStokes.LocalSignedRequest.movingStrip_domain {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (x : Point) : x ∈ (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL).domain ↔ x.2.1 ∈ U.carrier ∧ (profileMap coord x).1 ∈ Set.Ioo a b

theorem NavierStokes.LocalSignedRequest.movingStrip_majorant_eq {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (α C : ℝ) (k n : ℕ) (x : Point) (hx : (profileMap coord x).1 ∈ Set.Ioo a b) : have s := movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL; WeightedClasses.majorant s (fun (x : ℕ) (x_1 : Point) => s.zeta x_1) α C k n x = C * ε n ^ α * L n ^ k * WeightedRadialPrimitive.logWeight cL cR a b k (x.1 / √(MeanRankUpdate.chartQ coord x))

theorem NavierStokes.LocalSignedRequest.profileMap_positiveJets {coord rlo rhi : ℝ} (U : SlowRegion coord) {S : Set Point} (hS : S ⊆ PhysicalMeanDomain.slowDomain U.carrier) (hR : ∀ x ∈ S, x.1 ∈ Set.Icc rlo rhi) : BoundedPositiveJets (profileMap coord) S

theorem NavierStokes.LocalSignedRequest.inverseProfileMap_positiveJets {coord rlo rhi : ℝ} (U : SlowRegion coord) {S : Set Point} (hS : S ⊆ PhysicalMeanDomain.slowDomain U.carrier) (hR : ∀ x ∈ S, x.1 ∈ Set.Icc rlo rhi) : BoundedPositiveJets (inverseProfileMap coord) S

theorem NavierStokes.LocalSignedRequest.moving_radial_bounds {coord a b : ℝ} (U : SlowRegion coord) (ha : 0 < a) {x : Point} (hx : x.2.1 ∈ U.carrier) (hr : (profileMap coord x).1 ∈ Set.Ioo a b) : x.1 ∈ Set.Icc (√U.qlo * a) (√U.qhi * b)

theorem NavierStokes.LocalSignedRequest.meanClass_profileMap {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {α : ℝ} {f : ℕ → Point → V} (hf : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U.carrier ⋯) α f) : WeightedClasses.MeanClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : Point) => f n (profileMap coord x)

theorem NavierStokes.LocalSignedRequest.meanClass_inverseProfileMap {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {α : ℝ} {f : ℕ → Point → V} (hf : WeightedClasses.MeanClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U.carrier ⋯) α fun (n : ℕ) (x : PressureStream.Lift Plane) => f n (inverseProfileMap coord x)

theorem NavierStokes.LocalSignedRequest.compact_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (χ : ℝ → ℝ) (M : ℝ) (v : Plane) : PhysicalMeanDomain.FiberLocal (TransportPrimitive.compactIntegral χ M (0, v))

theorem NavierStokes.LocalSignedRequest.compact_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b M : ℝ} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (v : Plane) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanDomain.SupportedOn a b U f) : ContDiffOn ℝ (↑⊤) (TransportPrimitive.compactIntegral χ M (0, v) f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.LocalSignedRequest.meanClass_compact {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b c d cL cR : ℝ} (ha : 0 < a) (hac : a < c) (hcd : c < d) (hdb : d < b) (hcL : 0 < cL) (hcR : 0 < cR) (χ : ℝ → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ X ≤ c, χ X = 0) (hright : ∀ (X : ℝ), d ≤ X → χ X = 1) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → Plane) (f : ℕ → PressureStream.Lift S → ℝ) (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U)) (hs : ∀ (n : ℕ), PhysicalMeanDomain.SupportedOn a b U (f n)) (hclass : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData a b cL cR ha hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => TransportPrimitive.compactIntegral χ (M n) (0, v n) (f n)

The actual compact transport primitive preserves the radial flat weight on an arbitrary open slow domain. The cutoff is the supplied fixed cutoff.

theorem NavierStokes.LocalSignedRequest.sigma_fiberLocal {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (P : SignedStressPrimitive.Patch) (e : ℕ) : PhysicalMeanDomain.FiberLocal (SignedStressPrimitive.sigma P e)

theorem NavierStokes.LocalSignedRequest.sigma_contDiffOn {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (P : SignedStressPrimitive.Patch) (e : ℕ) {U : Set S} (hU : IsOpen U) {f : PressureStream.Lift S → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanDomain.SupportedOn P.a P.b U f) : ContDiffOn ℝ (↑⊤) (SignedStressPrimitive.sigma P e f) (PhysicalMeanDomain.slowDomain U)

theorem NavierStokes.LocalSignedRequest.meanClass_sigma {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (P : SignedStressPrimitive.Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U)) (hs : ∀ (n : ℕ), PhysicalMeanDomain.SupportedOn P.a P.b U (f n)) (hclass : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) => SignedStressPrimitive.sigma P e (f n)

theorem NavierStokes.LocalSignedRequest.meanClass_barSigma {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (P : SignedStressPrimitive.Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (U : Set S) (hU : IsOpen U) {α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U)) (hs : ∀ (n : ℕ), PhysicalMeanDomain.SupportedOn P.a P.b U (f n)) (hclass : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL U hU) α f) : WeightedClasses.MeanClass (PhysicalMeanDomain.localStripData P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL U hU) α fun (n : ℕ) (x : PressureStream.Lift S) => SignedStressPrimitive.barSigma P e (f n) (x.1, x.2.1)

noncomputable def NavierStokes.LocalSignedRequest.MovingSupport (a b coord : ℝ) (U : Set Plane) (f : Point → ℝ) : Prop

Support on the same moving shell used in the weight.

Equations

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

theorem NavierStokes.LocalSignedRequest.inverseProfile_source_smooth {coord : ℝ} (U : SlowRegion coord) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) : ContDiffOn ℝ (↑⊤) (fun (x : Point) => f (inverseProfileMap coord x)) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.LocalSignedRequest.inverseProfile_source_supported {coord a b : ℝ} (U : SlowRegion coord) {f : Point → ℝ} (hs : MovingSupport a b coord U.carrier f) : PhysicalMeanDomain.SupportedOn a b U.carrier fun (x : PressureStream.Lift Plane) => f (inverseProfileMap coord x)

theorem NavierStokes.LocalSignedRequest.chartKernel_unweighted {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {g : PhysicalCoordinateBounds.Point → ℝ} (hg : ContDiffOn ℝ (↑⊤) g PhysicalCoordinateBounds.positiveTime) : WeightedClasses.UnweightedClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 0 fun (x : ℕ) => MeanRankUpdate.chartKernel coord g

theorem NavierStokes.LocalSignedRequest.length_unweighted {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) : WeightedClasses.UnweightedClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 0 fun (x : ℕ) (x_1 : Point) => √(MeanRankUpdate.chartQ coord x_1)

theorem NavierStokes.LocalSignedRequest.qPower_unweighted {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (p : ℝ) : WeightedClasses.UnweightedClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) 0 fun (x : ℕ) (x_1 : Point) => MeanRankUpdate.chartQ coord x_1 ^ p

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_profile (P : SignedStressPrimitive.Patch) (e : ℕ) (coord : ℝ) (f : Point → ℝ) (x : Point) : SignedStressPrimitive.physicalBarSigma P e (SimilarityCoordinates.coordinateQ coord) f (x.1, x.2.1) = √(MeanRankUpdate.chartQ coord x) * SignedStressPrimitive.barSigma P e (fun (y : PressureStream.Lift Plane) => f (inverseProfileMap coord y)) ((profileMap coord x).1, x.2.1)

theorem NavierStokes.LocalSignedRequest.torusAverage_inverseProfileMap (coord : ℝ) (f : Point → ℝ) (x : Point) : MeanMomentBounds.liftedTorusAverage (fun (y : PressureStream.Lift Plane) => f (inverseProfileMap coord y)) x = MeanMomentBounds.liftedTorusAverage f (inverseProfileMap coord x)

theorem NavierStokes.LocalSignedRequest.meanClass_liftedTorusAverage {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hclass : WeightedClasses.MeanClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => MeanMomentBounds.liftedTorusAverage (f n)

theorem NavierStokes.LocalSignedRequest.meanClass_centered {coord : ℝ} (U : SlowRegion coord) (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hclass : WeightedClasses.MeanClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (movingStripData U a b cL cR ha hcL hcR ε L hε hεone hL) α fun (n : ℕ) => TemporalMeanUpdate.centered (f n)

theorem NavierStokes.LocalSignedRequest.meanClass_physicalBarSigma {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) {α : ℝ} {f : ℕ → Point → ℝ} (hf : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : ∀ (n : ℕ), MovingSupport P.a P.b coord U.carrier (f n)) (hclass : WeightedClasses.MeanClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α f) : WeightedClasses.MeanClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : Point) => SignedStressPrimitive.physicalBarSigma P e (SimilarityCoordinates.coordinateQ coord) (f n) (x.1, x.2.1)

The physical signed primitive, in the actual moving weight, costs no power of epsilon. The only constants come from the fixed profile and the bounded normalized slow region.

noncomputable def NavierStokes.LocalSignedRequest.requestedStress (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : ℕ → Point → SignedWaveUpdate.Vec2

Both components are computed from the same actual state.

Equations

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

noncomputable def NavierStokes.LocalSignedRequest.normalizedRequest (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : ℕ → Point → SignedWaveUpdate.Vec2

Normalized request, defined pointwise by (s.epsilon n)⁻¹ • requestedStress P coord c u n x.

Equations

• NavierStokes.LocalSignedRequest.normalizedRequest s P coord c u n x = (s.epsilon n)⁻¹ • NavierStokes.LocalSignedRequest.requestedStress P coord c u n x

theorem NavierStokes.LocalSignedRequest.normalizedRequest_class {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) {cL cR : ℝ} (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) (α : ℝ) (hθ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hsθ : ∀ (n : ℕ), MovingSupport P.a P.b coord U.carrier (u.thetaResidual c n)) (hsz : ∀ (n : ℕ), MovingSupport P.a P.b coord U.carrier (u.axialResidual c n)) (hcθ : WeightedClasses.MeanClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α (u.thetaResidual c)) (hcz : WeightedClasses.MeanClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α (u.axialResidual c)) (i : Fin 2) : WeightedClasses.MeanClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) (α - 1) fun (n : ℕ) (x : Point) => normalizedRequest (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) P coord c u n x i

theorem NavierStokes.LocalSignedRequest.normalizedRequest_frozen (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (v : Plane) : SignedWaveUpdate.FrozenAlong (0, 0, v) (normalizedRequest s P coord c u)

noncomputable def NavierStokes.LocalSignedRequest.fullRequest (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : ℕ → Point × ℝ → SignedWaveUpdate.Vec2

Genuine pullback to the full coefficient domain, including the angle.

Equations

• NavierStokes.LocalSignedRequest.fullRequest s P coord c u n x = NavierStokes.LocalSignedRequest.normalizedRequest s P coord c u n x.1

theorem NavierStokes.LocalSignedRequest.fullRequest_class (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {α : ℝ} (h : ∀ (i : Fin 2), WeightedClasses.MeanClass s α fun (n : ℕ) (x : Point) => normalizedRequest s P coord c u n x i) (i : Fin 2) : WeightedClasses.MeanClass (HarmonicWaveInteraction.productStrip s) α fun (n : ℕ) (x : Point × ℝ) => fullRequest s P coord c u n x i

theorem NavierStokes.LocalSignedRequest.fullRequest_angle_frozen (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : SignedWaveUpdate.FrozenAlong (0, 1) (fullRequest s P coord c u)

theorem NavierStokes.LocalSignedRequest.fullRequest_torus_frozen (s : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (v : Plane) : SignedWaveUpdate.FrozenAlong ((0, 0, v), 0) (fullRequest s P coord c u)

theorem NavierStokes.LocalSignedRequest.sigma_fiber_congr {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (P : SignedStressPrimitive.Patch) (e : ℕ) {f : ℝ × S → ℝ} {g : ℝ × T → ℝ} {s : S} {t : T} (he : ∀ (r : ℝ), f (r, s) = g (r, t)) (r : ℝ) : SignedStressPrimitive.sigma P e f (r, s) = SignedStressPrimitive.sigma P e g (r, t)

theorem NavierStokes.LocalSignedRequest.sigma_fiber_mul {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (P : SignedStressPrimitive.Patch) (e : ℕ) (u : ℝ) {f : ℝ × S → ℝ} {g : ℝ × T → ℝ} {s : S} {t : T} (he : ∀ (r : ℝ), f (r, s) = u * g (r, t)) (r : ℝ) : SignedStressPrimitive.sigma P e f (r, s) = u * SignedStressPrimitive.sigma P e g (r, t)

theorem NavierStokes.LocalSignedRequest.physicalSigma_scaled_fiber {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (P : SignedStressPrimitive.Patch) (e : ℕ) {q : S → ℝ} {q' : T → ℝ} {f : ℝ × S → ℝ} {g : ℝ × T → ℝ} {s : S} {t : T} {l : ℝ} (hl : 0 < l) (hq : 0 < q s) (u : ℝ) (hlength : √(q' t) = l * √(q s)) (he : ∀ (r : ℝ), f (r, s) = u * g (l * r, t)) (r : ℝ) : SignedStressPrimitive.physicalSigma P e q f (r, s) = u / l * SignedStressPrimitive.physicalSigma P e q' g (l * r, t)

Physical radial scaling changes a primitive by exactly one length factor.

theorem NavierStokes.LocalSignedRequest.torusAverage_coverPull_local {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (C : S →L[ℝ] T) (k : ℕ) (u : ℝ) {U : Set T} (hU : IsOpen U) {f : PressureStream.Lift T → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U f) (r : ℝ) {s : S} (hs : C s ∈ U) : PressureStream.torusAverage (MeanChartCompatibility.coverPull l C k u f) (r, s) = u * PressureStream.torusAverage f (l * r, C s)

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_chart {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (P : SignedStressPrimitive.Patch) (e : ℕ) {q : S → ℝ} {q' : T → ℝ} {f : PressureStream.Lift S → ℝ} {g : PressureStream.Lift T → ℝ} {s : S} {l : ℝ} (hl : 0 < l) (hq : 0 < q s) (C : S →L[ℝ] T) (k : ℕ) (u : ℝ) {U : Set T} (hU : IsOpen U) (hs : C s ∈ U) (hg : ContDiffOn ℝ (↑⊤) g (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U g) (hlength : √(q' (C s)) = l * √(q s)) (he : ∀ (r : ℝ) (Y : PressureStream.Plane), f (r, s, Y) = u * g (l * r, C s, (TemporalMeanUpdate.coverMap k) Y)) (r : ℝ) : SignedStressPrimitive.physicalBarSigma P e q f (r, s) = u / l * SignedStressPrimitive.physicalBarSigma P e q' g (l * r, C s)

One physical request has all chart views. Only the target slow fiber needs regularity and periodicity.

noncomputable def NavierStokes.LocalSignedRequest.physicalRequestedStress {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (P : SignedStressPrimitive.Patch) (q : S → ℝ) (Fθ Fz : PressureStream.Lift S → ℝ) (x : ℝ × S) : SignedWaveUpdate.Vec2

This field has no band index: every normalized request below represents this same physical signed stress.

Equations

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

theorem NavierStokes.LocalSignedRequest.stress_unit_factor {Q : ℝ} (hQ : 0 < Q) (A : ℝ) : Q ^ (2 * A) * (Q ^ (-(2 * A + 1 / 2)) / Q ^ (-(1 / 2))) = 1

theorem NavierStokes.LocalSignedRequest.normalizedRequest_represents {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (s : WeightedClasses.StripData Point) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) {Q : ℝ} (hQ : 0 < Q) (A : ℝ) (q : S → ℝ) (Fθ Fz : PressureStream.Lift S → ℝ) (C : S →L[ℝ] Plane) (k : ℕ) (t : S) (ht : C t ∈ U.carrier) (hqt : 0 < q t) (hθ : ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hz : ContDiffOn ℝ (↑⊤) (u.axialResidual c n) (PhysicalMeanDomain.slowDomain U.carrier)) (hpθ : PhysicalMeanDomain.PeriodicOn U.carrier (u.thetaResidual c n)) (hpz : PhysicalMeanDomain.PeriodicOn U.carrier (u.axialResidual c n)) (hlength : √(SimilarityCoordinates.coordinateQ coord (C t)) = Q ^ (-(1 / 2)) * √(q t)) (heθ : ∀ (r : ℝ) (Y : PressureStream.Plane), Fθ (r, t, Y) = Q ^ (-(2 * A + 1 / 2)) * u.thetaResidual c n (Q ^ (-(1 / 2)) * r, C t, (TemporalMeanUpdate.coverMap k) Y)) (hez : ∀ (r : ℝ) (Y : PressureStream.Plane), Fz (r, t, Y) = Q ^ (-(2 * A + 1 / 2)) * u.axialResidual c n (Q ^ (-(1 / 2)) * r, C t, (TemporalMeanUpdate.coverMap k) Y)) (r : ℝ) (Y : Plane) : normalizedRequest s P coord c u n (Q ^ (-(1 / 2)) * r, C t, Y) = (s.epsilon n)⁻¹ • Q ^ (2 * A) • physicalRequestedStress P q Fθ Fz (r, t)

Exact Q-normalization of one physical primitive. The hypotheses refer to the actual represented source, not to the desired stress or its bounds.

theorem NavierStokes.LocalSignedRequest.physicalSigma_fiber_congr {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (P : SignedStressPrimitive.Patch) (e : ℕ) {q : S → ℝ} {q' : T → ℝ} {f : ℝ × S → ℝ} {g : ℝ × T → ℝ} {s : S} {t : T} (hq : q s = q' t) (he : ∀ (r : ℝ), f (r, s) = g (r, t)) (r : ℝ) : SignedStressPrimitive.physicalSigma P e q f (r, s) = SignedStressPrimitive.physicalSigma P e q' g (r, t)

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_eq_negative_primitive {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : MovingSupport P.a P.b coord U.carrier f) {s : Plane} (hsp : s ∈ U.carrier) (r : ℝ) : SignedStressPrimitive.physicalBarSigma P e (SimilarityCoordinates.coordinateQ coord) f (r, s) = (-∫ (t : ℝ) in 0..r, t ^ e * SignedStressPrimitive.physicalAdjusted P e (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage f) (t, s)) / r ^ e

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_angular_divergence {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : MovingSupport P.a P.b coord U.carrier f) {s : Plane} (hsp : s ∈ U.carrier) {r : ℝ} (hr : 0 < r) : IntegratedMeanBalances.radialDivergence 2 (fun (t : ℝ) => SignedStressPrimitive.physicalBarSigma P 2 (SimilarityCoordinates.coordinateQ coord) f (t, s)) r = -SignedStressPrimitive.physicalAdjusted P 2 (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage f) (r, s)

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_axial_divergence {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : MovingSupport P.a P.b coord U.carrier f) {s : Plane} (hsp : s ∈ U.carrier) {r : ℝ} (hr : 0 < r) : IntegratedMeanBalances.radialDivergence 1 (fun (t : ℝ) => SignedStressPrimitive.physicalBarSigma P 1 (SimilarityCoordinates.coordinateQ coord) f (t, s)) r = -SignedStressPrimitive.physicalAdjusted P 1 (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage f) (r, s)

theorem NavierStokes.LocalSignedRequest.physicalAdjusted_moment_zero {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : MovingSupport P.a P.b coord U.carrier f) {s : Plane} (hsp : s ∈ U.carrier) : SignedStressPrimitive.mass e (SignedStressPrimitive.physicalAdjusted P e (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage f)) s = 0

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_supported {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : MovingSupport P.a P.b coord U.carrier f) : MovingSupport P.a P.b coord U.carrier fun (x : Point) => SignedStressPrimitive.physicalBarSigma P e (SimilarityCoordinates.coordinateQ coord) f (x.1, x.2.1)

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_slice_compact {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : MovingSupport P.a P.b coord U.carrier f) {s : Plane} (hsp : s ∈ U.carrier) : HasCompactSupport fun (r : ℝ) => SignedStressPrimitive.physicalBarSigma P e (SimilarityCoordinates.coordinateQ coord) f (r, s)

theorem NavierStokes.LocalSignedRequest.physicalBarSigma_contDiffOn {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {f : Point → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U.carrier)) (hs : MovingSupport P.a P.b coord U.carrier f) : ContDiffOn ℝ (↑⊤) (fun (x : Point) => SignedStressPrimitive.physicalBarSigma P e (SimilarityCoordinates.coordinateQ coord) f (x.1, x.2.1)) (PhysicalMeanDomain.slowDomain U.carrier)

theorem NavierStokes.LocalSignedRequest.physicalDensity_meanClass {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) : WeightedClasses.MeanClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) 0 fun (x : ℕ) (x_1 : Point) => SignedStressPrimitive.physicalDensity P e (SimilarityCoordinates.coordinateQ coord) (x_1.1, x_1.2.1)

theorem NavierStokes.LocalSignedRequest.fderiv_slowLift (D : Plane → ℝ) (x : Point) (v : Plane) (hD : DifferentiableAt ℝ D x.2.1) : (fderiv ℝ (fun (p : Point) => D p.2.1) x) (0, v, 0) = (fderiv ℝ D x.2.1) v

theorem NavierStokes.LocalSignedRequest.physicalBump_improvedClass_of_moment {coord : ℝ} (U : SlowRegion coord) (P : SignedStressPrimitive.Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε L : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hL : ∀ (n : ℕ), 1 ≤ L n) (F : ℕ → Point → ℝ) (D : ℕ → Plane → ℝ) (v : Plane) (α : ℝ) (hD : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (D n) U.carrier) (hclass : WeightedClasses.UnweightedClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) α fun (n : ℕ) (x : Point) => D n x.2.1) (hmoment : ∀ (n : ℕ), ∀ s ∈ U.carrier, SignedStressPrimitive.mass e (PressureStream.torusAverage (F n)) s = ε n * (fderiv ℝ (D n) s) v) : WeightedClasses.MeanClass (movingStripData U P.a P.b cL cR ⋯ hcL hcR ε L hε hεone hL) (α + 1) fun (n : ℕ) (x : Point) => SignedStressPrimitive.physicalBump P e (SimilarityCoordinates.coordinateQ coord) (PressureStream.torusAverage (F n)) (x.1, x.2.1)

A measured moment equal to epsilon times a slow derivative yields the extra epsilon in the actual removed physical bump, in the same moving weight.