Physical power-coordinate pullback of the weighted radial inverse

The power coordinate is U = R^d on a fixed positive annulus. Smooth positive regularizations below the annulus make every source and output a genuine globally defined smooth function. They agree with the prescribed power maps where the source or the output can be nonzero.

Uniform flat-weight estimates for radial primitives

The initial coordinate is additive distance from the left endpoint of a fixed interval (0,L). The constants in the estimates are independent of the point approaching either endpoint and of any auxiliary shifts in the source.

def NavierStokes.WeightedRadialPrimitive.delta (L x : ℝ) : ℝ

Delta, given by min 1 (min x (L - x)).

Equations

• NavierStokes.WeightedRadialPrimitive.delta L x = min 1 (min x (L - x))

noncomputable def NavierStokes.WeightedRadialPrimitive.zeta (cL cR L x : ℝ) : ℝ

Zeta, given by edge cL x * edge cR (L - x).

Equations

• NavierStokes.WeightedRadialPrimitive.zeta cL cR L x = NavierStokes.FlatCutoff.edge cL x * NavierStokes.FlatCutoff.edge cR (L - x)

noncomputable def NavierStokes.WeightedRadialPrimitive.weight (cL cR L : ℝ) (m : ℕ) (x : ℝ) : ℝ

Weight, given by zeta cL cR L x / delta L x ^ m.

Equations

• NavierStokes.WeightedRadialPrimitive.weight cL cR L m x = NavierStokes.WeightedRadialPrimitive.zeta cL cR L x / NavierStokes.WeightedRadialPrimitive.delta L x ^ m

noncomputable def NavierStokes.WeightedRadialPrimitive.singleWeight (c : ℝ) (m : ℕ) (x : ℝ) : ℝ

Single weight, given by edge c x / x ^ m.

Equations

• NavierStokes.WeightedRadialPrimitive.singleWeight c m x = NavierStokes.FlatCutoff.edge c x / x ^ m

theorem NavierStokes.WeightedRadialPrimitive.delta_pos {L x : ℝ} (hx : x ∈ Set.Ioo 0 L) : 0 < delta L x

theorem NavierStokes.WeightedRadialPrimitive.delta_le_one (L x : ℝ) : delta L x ≤ 1

theorem NavierStokes.WeightedRadialPrimitive.delta_le_left (L x : ℝ) : delta L x ≤ x

theorem NavierStokes.WeightedRadialPrimitive.delta_le_right (L x : ℝ) : delta L x ≤ L - x

theorem NavierStokes.WeightedRadialPrimitive.zeta_pos (cL cR : ℝ) {L x : ℝ} (hx : x ∈ Set.Ioo 0 L) : 0 < zeta cL cR L x

theorem NavierStokes.WeightedRadialPrimitive.zeta_continuous {cL cR : ℝ} (hL : 0 < cL) (hR : 0 < cR) (L : ℝ) : Continuous (zeta cL cR L)

theorem NavierStokes.WeightedRadialPrimitive.weight_pos (cL cR : ℝ) (m : ℕ) {L x : ℝ} (hx : x ∈ Set.Ioo 0 L) : 0 < weight cL cR L m x

theorem NavierStokes.WeightedRadialPrimitive.zeta_le_weight (cL cR : ℝ) (m : ℕ) {L x : ℝ} (hx : x ∈ Set.Ioo 0 L) : zeta cL cR L x ≤ weight cL cR L m x

theorem NavierStokes.WeightedRadialPrimitive.edge_mono {c : ℝ} (hc : 0 ≤ c) : Monotone (FlatCutoff.edge c)

Single-edge monotonicity is proved from the exponential formula.

theorem NavierStokes.WeightedRadialPrimitive.edge_le_one {c : ℝ} (hc : 0 ≤ c) (x : ℝ) : FlatCutoff.edge c x ≤ 1

theorem NavierStokes.WeightedRadialPrimitive.singleWeight_nonneg (c : ℝ) (m : ℕ) (x : ℝ) : 0 ≤ singleWeight c m x

theorem NavierStokes.WeightedRadialPrimitive.singleWeight_continuous {c : ℝ} (hc : 0 < c) (m : ℕ) : Continuous (singleWeight c m)

theorem NavierStokes.WeightedRadialPrimitive.single_primitive_uniform {c : ℝ} (hc : 0 < c) (m : ℕ) {R : ℝ} (hR : 0 < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 0 < x → x ≤ R → intervalIntegral (singleWeight c m) 0 x MeasureTheory.volume ≤ C * singleWeight c m x

Compactness of the actual transformed improper integral gives one constant for the primitive, uniformly down to the flat endpoint.

theorem NavierStokes.WeightedRadialPrimitive.delta_left_half {L x : ℝ} (hx : x ≤ L / 2) : delta L x = min 1 x

theorem NavierStokes.WeightedRadialPrimitive.weight_le_left_majorant {cL cR L x : ℝ} (hcR : 0 ≤ cR) (m : ℕ) (hx : 0 < x) (hxL : x ≤ L / 2) : weight cL cR L m x ≤ singleWeight cL 0 x + singleWeight cL m x

The two-edge weight on the left half is controlled by two integrable single-edge weights. This includes all powers of the clipped edge distance.

theorem NavierStokes.WeightedRadialPrimitive.weight_reflect (cL cR L : ℝ) (m : ℕ) (x : ℝ) : weight cL cR L m (L - x) = weight cR cL L m x

theorem NavierStokes.WeightedRadialPrimitive.left_single_le_weight {cL cR L x : ℝ} (hcR : 0 ≤ cR) (m : ℕ) (hx : 0 < x) (hxL : x ≤ L / 2) : singleWeight cL m x ≤ (FlatCutoff.edge cR (L / 2))⁻¹ * weight cL cR L m x

Dividing by the opposite-edge value at the midpoint is a fixed constant, independent of the variable tending to the left endpoint.

theorem NavierStokes.WeightedRadialPrimitive.left_base_le_weight {cL cR L x : ℝ} (hcR : 0 ≤ cR) (m : ℕ) (hx : 0 < x) (hxL : x ≤ L / 2) : singleWeight cL 0 x ≤ (FlatCutoff.edge cR (L / 2))⁻¹ * weight cL cR L m x

noncomputable def NavierStokes.WeightedRadialPrimitive.wholeMajorant (cL cR L : ℝ) (m : ℕ) (x : ℝ) : ℝ

Whole majorant, given by `singleWeight cL 0 x + singleWeight cL m x + (singleWeight cR 0 (L

• x) + singleWeight cR m (L - x))`.

Equations

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

theorem NavierStokes.WeightedRadialPrimitive.weight_le_wholeMajorant {cL cR L x : ℝ} (hcL : 0 ≤ cL) (hcR : 0 ≤ cR) (m : ℕ) (hx : x ∈ Set.Ioo 0 L) : weight cL cR L m x ≤ wholeMajorant cL cR L m x

theorem NavierStokes.WeightedRadialPrimitive.wholeMajorant_continuous {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (L : ℝ) (m : ℕ) : Continuous (wholeMajorant cL cR L m)

theorem NavierStokes.WeightedRadialPrimitive.weight_uniform_bound {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (L : ℝ) (m : ℕ) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ x ∈ Set.Ioo 0 L, weight cL cR L m x ≤ D

A single global bound for the weighted envelope on the whole finite shell.

theorem NavierStokes.WeightedRadialPrimitive.middle_weight_lower_bound {cL cR L ρ : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hρ : 0 < ρ) : ∃ (d : ℝ), 0 < d ∧ ∀ (m : ℕ), ∀ x ∈ Set.Icc ρ (L - ρ), d ≤ weight cL cR L m x

theorem NavierStokes.WeightedRadialPrimitive.left_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {cL cR L : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ → V) (A : ℝ), 0 ≤ A → (∀ s ∈ Set.Ioo 0 L, ‖f s‖ ≤ A * weight cL cR L m s) → ∀ (x : ℝ), 0 < x → x ≤ L / 2 → ‖intervalIntegral f 0 x MeasureTheory.volume‖ ≤ K * A * weight cL cR L m x

The left inverse estimate is uniform at the endpoint, with no loss of the polynomial edge exponent. It applies to arbitrary Banach-valued sources.

theorem NavierStokes.WeightedRadialPrimitive.right_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {cL cR L : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ → V) (A : ℝ), 0 ≤ A → (∀ s ∈ Set.Ioo 0 L, ‖f s‖ ≤ A * weight cL cR L m s) → ∀ (x : ℝ), L / 2 ≤ x → x < L → ‖intervalIntegral f x L MeasureTheory.volume‖ ≤ K * A * weight cL cR L m x

Reflection gives the corresponding endpoint-uniform right inverse bound.

theorem NavierStokes.WeightedRadialPrimitive.interval_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {cL cR L : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (m : ℕ) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (f : ℝ → V) (A : ℝ), 0 ≤ A → (∀ s ∈ Set.Ioo 0 L, ‖f s‖ ≤ A * weight cL cR L m s) → ∀ (a b : ℝ), 0 ≤ a → a ≤ b → b ≤ L → ‖intervalIntegral f a b MeasureTheory.volume‖ ≤ D * A

Uniform total and partial mass bounds on the finite shell. Endpoint values of the source are immaterial to this Lebesgue-integral statement.

noncomputable def NavierStokes.WeightedRadialPrimitive.compactPrimitive {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (χ : ℝ → ℝ) (f : ℝ → V) (L x : ℝ) : V

Compact primitive, given by intervalIntegral f 0 x volume - χ x • intervalIntegral f 0 L volume.

Equations

• NavierStokes.WeightedRadialPrimitive.compactPrimitive χ f L x = intervalIntegral f 0 x MeasureTheory.volume - χ x • intervalIntegral f 0 L MeasureTheory.volume

theorem NavierStokes.WeightedRadialPrimitive.compact_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {cL cR L ρ : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (hL : 0 < L) (hρ : 0 < ρ) (hρL : ρ ≤ L / 2) (m : ℕ) (χ : ℝ → ℝ) (hχ : ∀ (x : ℝ), |χ x| ≤ 1) (hleft : ∀ x ≤ ρ, χ x = 0) (hright : ∀ (x : ℝ), L - ρ ≤ x → χ x = 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ → V), Continuous f → ∀ (A : ℝ), 0 ≤ A → (∀ s ∈ Set.Ioo 0 L, ‖f s‖ ≤ A * weight cL cR L m s) → ∀ x ∈ Set.Ioo 0 L, ‖compactPrimitive χ f L x‖ ≤ K * A * weight cL cR L m x

The actual compactified primitive preserves the same two-edge weighted envelope. The cutoff is only required to have two plateaus and remain bounded; no monotonicity of the weight or inverse estimate is assumed.

Pullback to logarithmic edge distances on a fixed positive annulus

noncomputable def NavierStokes.WeightedRadialPrimitive.logLength (a b : ℝ) : ℝ

Log length, given by Real.log (b / a).

Equations

• NavierStokes.WeightedRadialPrimitive.logLength a b = Real.log (b / a)

noncomputable def NavierStokes.WeightedRadialPrimitive.logPosition (a X : ℝ) : ℝ

Log position, given by Real.log (X / a).

Equations

• NavierStokes.WeightedRadialPrimitive.logPosition a X = Real.log (X / a)

noncomputable def NavierStokes.WeightedRadialPrimitive.logWeight (cL cR a b : ℝ) (m : ℕ) (X : ℝ) : ℝ

Log weight, given by weight cL cR (logLength a b) m (logPosition a X).

Equations

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

theorem NavierStokes.WeightedRadialPrimitive.logLength_pos {a b : ℝ} (ha : 0 < a) (hab : a < b) : 0 < logLength a b

theorem NavierStokes.WeightedRadialPrimitive.logPosition_mem {a b X : ℝ} (ha : 0 < a) (hX : X ∈ Set.Ioo a b) : logPosition a X ∈ Set.Ioo 0 (logLength a b)

theorem NavierStokes.WeightedRadialPrimitive.log_remaining {a b X : ℝ} (ha : 0 < a) (hX : X ∈ Set.Ioo a b) : logLength a b - logPosition a X = Real.log (b / X)

theorem NavierStokes.WeightedRadialPrimitive.logWeight_formula {a b X : ℝ} (ha : 0 < a) (hX : X ∈ Set.Ioo a b) (cL cR : ℝ) (m : ℕ) : logWeight cL cR a b m X = Real.exp (-cL / Real.log (X / a) ^ 2 - cR / Real.log (b / X) ^ 2) / min 1 (min (Real.log (X / a)) (Real.log (b / X))) ^ m

The weight is exactly the manuscript's two logarithmic-edge exponential, with its clipped inverse-edge power.

noncomputable def NavierStokes.WeightedRadialPrimitive.expCoordinate (a s : ℝ) : ℝ

Exp coordinate, given by a * Real.exp s.

Equations

• NavierStokes.WeightedRadialPrimitive.expCoordinate a s = a * Real.exp s

theorem NavierStokes.WeightedRadialPrimitive.expCoordinate_logPosition {a X : ℝ} (ha : 0 < a) (hX : 0 < X) : expCoordinate a (logPosition a X) = X

theorem NavierStokes.WeightedRadialPrimitive.logPosition_expCoordinate {a : ℝ} (ha : 0 < a) (s : ℝ) : logPosition a (expCoordinate a s) = s

theorem NavierStokes.WeightedRadialPrimitive.expCoordinate_mem {a b s : ℝ} (ha : 0 < a) (hab : a < b) (hs : s ∈ Set.Ioo 0 (logLength a b)) : expCoordinate a s ∈ Set.Ioo a b

noncomputable def NavierStokes.WeightedRadialPrimitive.expPullback {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℝ) (f : ℝ → V) (s : ℝ) : V

Exp pullback, given by expCoordinate a s • f (expCoordinate a s).

Equations

• NavierStokes.WeightedRadialPrimitive.expPullback a f s = NavierStokes.WeightedRadialPrimitive.expCoordinate a s • f (NavierStokes.WeightedRadialPrimitive.expCoordinate a s)

theorem NavierStokes.WeightedRadialPrimitive.expPullback_integral {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℝ) (f : ℝ → V) (hf : Continuous f) (l r : ℝ) : intervalIntegral (expPullback a f) l r MeasureTheory.volume = intervalIntegral f (expCoordinate a l) (expCoordinate a r) MeasureTheory.volume

Actual change of variables, including the radial integration Jacobian.

theorem NavierStokes.WeightedRadialPrimitive.expPullback_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR A : ℝ} (ha : 0 < a) (hab : a < b) (m : ℕ) (f : ℝ → V) (_hA : 0 ≤ A) (hf : ∀ X ∈ Set.Ioo a b, ‖f X‖ ≤ A * logWeight cL cR a b m X) (s : ℝ) : s ∈ Set.Ioo 0 (logLength a b) → ‖expPullback a f s‖ ≤ b * A * weight cL cR (logLength a b) m s

theorem NavierStokes.WeightedRadialPrimitive.log_left_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ → V), Continuous f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ‖f X‖ ≤ A * logWeight cL cR a b m X) → ∀ X ∈ Set.Ioo a b, logPosition a X ≤ logLength a b / 2 → ‖intervalIntegral f a X MeasureTheory.volume‖ ≤ K * A * logWeight cL cR a b m X

Left logarithmic-edge estimate in the original positive radial variable. The extra constant is only the fixed upper radial endpoint b.

theorem NavierStokes.WeightedRadialPrimitive.log_right_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ → V), Continuous f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ‖f X‖ ≤ A * logWeight cL cR a b m X) → ∀ X ∈ Set.Ioo a b, logLength a b / 2 ≤ logPosition a X → ‖intervalIntegral f X b MeasureTheory.volume‖ ≤ K * A * logWeight cL cR a b m X

Right logarithmic-edge estimate in the original positive radial variable.

theorem NavierStokes.WeightedRadialPrimitive.log_interval_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (m : ℕ) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (f : ℝ → V) (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ‖f X‖ ≤ A * logWeight cL cR a b m X) → ∀ (l r : ℝ), a ≤ l → l ≤ r → r ≤ b → ‖intervalIntegral f l r MeasureTheory.volume‖ ≤ D * A

The entire weighted source has uniformly bounded mass on the positive annulus. This also bounds every interior subinterval.

noncomputable def NavierStokes.WeightedRadialPrimitive.logCompactPrimitive {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (χ : ℝ → ℝ) (f : ℝ → V) (a b X : ℝ) : V

Log compact primitive, given by intervalIntegral f a X volume - χ (logPosition a X) • intervalIntegral f a b volume.

Equations

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

theorem NavierStokes.WeightedRadialPrimitive.log_compact_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR ρ : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (hρ : 0 < ρ) (hρL : ρ ≤ logLength a b / 2) (m : ℕ) (χ : ℝ → ℝ) (hχ : ∀ (x : ℝ), |χ x| ≤ 1) (hleft : ∀ x ≤ ρ, χ x = 0) (hright : ∀ (x : ℝ), logLength a b - ρ ≤ x → χ x = 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ → V), Continuous f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ‖f X‖ ≤ A * logWeight cL cR a b m X) → ∀ X ∈ Set.Ioo a b, ‖logCompactPrimitive χ f a b X‖ ≤ K * A * logWeight cL cR a b m X

The compactified primitive preserves the explicit logarithmic two-edge weight uniformly on the whole positive annulus.

Physical cutoffs and auxiliary shifts

noncomputable def NavierStokes.WeightedRadialPrimitive.radialCompactPrimitive {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (χ : ℝ → ℝ) (f : ℝ → V) (a b X : ℝ) : V

Radial compact primitive, given by intervalIntegral f a X volume - χ X • intervalIntegral f a b volume.

Equations

• NavierStokes.WeightedRadialPrimitive.radialCompactPrimitive χ f a b X = intervalIntegral f a X MeasureTheory.volume - χ X • intervalIntegral f a b MeasureTheory.volume

theorem NavierStokes.WeightedRadialPrimitive.exists_log_plateau_width {a b c d : ℝ} (ha : 0 < a) (hac : a < c) (hcd : c < d) (hdb : d < b) (χ : ℝ → ℝ) (hleft : ∀ X ≤ c, χ X = 0) (hright : ∀ (X : ℝ), d ≤ X → χ X = 1) : ∃ (ρ : ℝ), 0 < ρ ∧ ρ ≤ logLength a b / 2 ∧ (∀ s ≤ ρ, χ (expCoordinate a s) = 0) ∧ ∀ (s : ℝ), logLength a b - ρ ≤ s → χ (expCoordinate a s) = 1

Any fixed pair of interior physical plateau thresholds gives positive logarithmic collars. This derives the collars from the endpoints.

theorem NavierStokes.WeightedRadialPrimitive.radial_compact_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ 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) (m : ℕ) (χ : ℝ → ℝ) (hχ : ∀ (X : ℝ), |χ X| ≤ 1) (hleft : ∀ X ≤ c, χ X = 0) (hright : ∀ (X : ℝ), d ≤ X → χ X = 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ → V), Continuous f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ‖f X‖ ≤ A * logWeight cL cR a b m X) → ∀ X ∈ Set.Ioo a b, ‖radialCompactPrimitive χ f a b X‖ ≤ K * A * logWeight cL cR a b m X

The cutoff can be specified directly in the physical radial coordinate. No logarithmic cutoff regularity or assumed inverse bound is required.

def NavierStokes.WeightedRadialPrimitive.radialSlice {V : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) (f : ℝ × E → V) (z : ℝ × E) (s : ℝ) : V

A source slice along the actual affine shifted radial characteristic.

Equations

• NavierStokes.WeightedRadialPrimitive.radialSlice M v f z s = f (s, z.2 + (M * (s - z.1)) • v)

theorem NavierStokes.WeightedRadialPrimitive.radialSlice_continuous {V : Type u_1} [NormedAddCommGroup V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → V} (hf : Continuous f) (M : ℝ) (v : E) (z : ℝ × E) : Continuous (radialSlice M v f z)

theorem NavierStokes.WeightedRadialPrimitive.shifted_radial_compact_primitive_uniform {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b c d cL cR : ℝ} (ha : 0 < a) (hac : a < c) (hcd : c < d) (hdb : d < b) (hcL : 0 < cL) (hcR : 0 < cR) (m : ℕ) (χ : ℝ → ℝ) (hχ : ∀ (X : ℝ), |χ X| ≤ 1) (hleft : ∀ X ≤ c, χ X = 0) (hright : ∀ (X : ℝ), d ≤ X → χ X = 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : E) (f : ℝ × E → V), Continuous f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ∀ (Y : E), ‖f (X, Y)‖ ≤ A * logWeight cL cR a b m X) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo a b → ‖radialCompactPrimitive χ (radialSlice M v f z) a b z.1‖ ≤ K * A * logWeight cL cR a b m z.1

Auxiliary translation does not change a radial bound that is uniform in the auxiliary variable. Constants are independent of M, v, and the base point.

The actual transport operator

theorem NavierStokes.WeightedRadialPrimitive.compactIntegral_eq_radialCompactPrimitive {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b M : ℝ} {v : E} {f : ℝ × E → V} (χ : ℝ → ℝ) (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : TransportPrimitive.compactIntegral χ M v f z = radialCompactPrimitive χ (radialSlice M v f z) a b z.1

theorem NavierStokes.WeightedRadialPrimitive.transport_compact_primitive_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ 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) (m : ℕ) (χ : ℝ → ℝ) (hχ : ∀ (X : ℝ), |χ X| ≤ 1) (hleft : ∀ X ≤ c, χ X = 0) (hright : ∀ (X : ℝ), d ≤ X → χ X = 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : E) (f : ℝ × E → V), Continuous f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ∀ (Y : E), ‖f (X, Y)‖ ≤ A * logWeight cL cR a b m X) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo a b → ‖TransportPrimitive.compactIntegral χ M v f z‖ ≤ K * A * logWeight cL cR a b m z.1

A uniform weighted inverse bound for the manuscript's actual shifted, compactified transport primitive. All shifts are quantified after the constant.

theorem NavierStokes.WeightedRadialPrimitive.canonical_transport_compact_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : E) (f : ℝ × E → V), Continuous f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ∀ (Y : E), ‖f (X, Y)‖ ≤ A * logWeight cL cR a b m X) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo a b → ‖TransportPrimitive.compactIntegral (TransportPrimitive.interiorCutoff a b) M v f z‖ ≤ K * A * logWeight cL cR a b m z.1

The cutoff itself is the explicit smooth transition constructed in TransportPrimitive; there is no cutoff-existence hypothesis.

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

The uncorrected past primitive obeys the left weighted estimate uniformly in every auxiliary shift.

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

The future primitive obeys the right weighted estimate.

theorem NavierStokes.WeightedRadialPrimitive.transport_mass_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (m : ℕ) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (M : ℝ) (v : E) (f : ℝ × E → V), Continuous f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → (∀ X ∈ Set.Ioo a b, ∀ (Y : E), ‖f (X, Y)‖ ≤ A * logWeight cL cR a b m X) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo a b → ‖TransportPrimitive.pastIntegral M v f z‖ ≤ D * A ∧ ‖TransportPrimitive.totalIntegral M v f z‖ ≤ D * A

A common bound for past and total mass, uniform in every shift and in the point in the annulus. It is used only on a compact interior collar.

theorem NavierStokes.WeightedRadialPrimitive.cutoff_finiteJet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (χ : ℝ → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (m : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ j ≤ m, ∀ (z : ℝ × E), z.1 ∈ Set.Icc a b → ‖iteratedFDeriv ℝ j (fun (y : ℝ × E) => χ y.1) z‖ ≤ B

A smooth scalar radial cutoff has bounded actual Fréchet jets on the entire strip, including its unbounded auxiliary directions.

theorem NavierStokes.WeightedRadialPrimitive.compact_jet_eq_past_on_left {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a M ρ : ℝ} {v : E} {f : ℝ × E → V} {χ : ℝ → ℝ} (ha : 0 < a) (hleft : ∀ s ≤ ρ, χ (expCoordinate a s) = 0) (z : ℝ × E) (hz : 0 < z.1) (hzρ : logPosition a z.1 < ρ) (j : ℕ) : iteratedFDeriv ℝ j (TransportPrimitive.compactIntegral χ M v f) z = iteratedFDeriv ℝ j (TransportPrimitive.pastIntegral M v f) z

On an open left logarithmic collar, every actual derivative of the compactified operator equals the corresponding derivative of the past integral.

theorem NavierStokes.WeightedRadialPrimitive.compact_jet_eq_neg_future_on_right {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b M ρ : ℝ} {v : E} {f : ℝ × E → V} {χ : ℝ → ℝ} (ha : 0 < a) (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (hright : ∀ (s : ℝ), logLength a b - ρ ≤ s → χ (expCoordinate a s) = 1) (z : ℝ × E) (hz : 0 < z.1) (hzρ : logLength a b - ρ < logPosition a z.1) (j : ℕ) : iteratedFDeriv ℝ j (TransportPrimitive.compactIntegral χ M v f) z = -iteratedFDeriv ℝ j (TransportPrimitive.futureIntegral M v f) z

On an open right logarithmic collar the compactified operator equals the negative future integral, including all its actual derivatives.

theorem NavierStokes.WeightedRadialPrimitive.transport_compact_finiteJets_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [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 : E) (f : ℝ × E → V), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → (∀ j ≤ m, ∀ X ∈ Set.Ioo a b, ∀ (Y : E), ‖iteratedFDeriv ℝ j f (X, Y)‖ ≤ A * logWeight cL cR a b p X) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo a b → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (TransportPrimitive.compactIntegral χ M v f) z‖ ≤ K * A * logWeight cL cR a b p z.1

Every finite prefix of actual Fréchet derivatives of the compactified transport inverse preserves the same flat radial envelope. The estimate is uniform in the shift and in all auxiliary variables.

theorem NavierStokes.WeightedRadialPrimitive.canonical_transport_finiteJets_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [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 : E) (f : ℝ × E → V), ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → ∀ (A : ℝ), 0 ≤ A → (∀ j ≤ m, ∀ X ∈ Set.Ioo a b, ∀ (Y : E), ‖iteratedFDeriv ℝ j f (X, Y)‖ ≤ A * logWeight cL cR a b p X) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo a b → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (TransportPrimitive.compactIntegral (TransportPrimitive.interiorCutoff a b) M v f) z‖ ≤ K * A * logWeight cL cR a b p z.1

The manuscript's all-jet mean class on a concrete annulus

noncomputable def NavierStokes.WeightedRadialPrimitive.logStripData {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) : WeightedClasses.StripData (ℝ × E)

A concrete StripData: the radial domain and both weights are explicit; the only inputs beyond the annulus are the positive band scales.

Equations

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

theorem NavierStokes.WeightedRadialPrimitive.logStrip_majorant_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (α C : ℝ) (p n : ℕ) (z : ℝ × E) (hz : z.1 ∈ Set.Ioo a b) : WeightedClasses.majorant (logStripData a b cL cR ha hcL hcR ε S hε hεone hS) (fun (x : ℕ) (y : ℝ × E) => (logStripData a b cL cR ha hcL hcR ε S hε hεone hS).zeta y) α C p n z = C * ε n ^ α * S n ^ p * logWeight cL cR a b p z.1

On the concrete strip, the library majorant is exactly a band amplitude times the explicit logarithmic radial weight.

theorem NavierStokes.WeightedRadialPrimitive.meanClass_canonical_transport {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → E) (f : ℕ → ℝ × E → V) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) : WeightedClasses.MeanClass (logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) => TransportPrimitive.compactIntegral (TransportPrimitive.interiorCutoff a b) (M n) (v n) (f n)

The concrete compactified shifted inverse preserves the all-jet mean class M_α on the explicit logarithmic annulus. Both radial support and global smoothness of the input are named hypotheses; neither the inverse estimate nor smoothness of the output is assumed. The bandwise shifts may be arbitrary.

theorem NavierStokes.WeightedRadialPrimitive.supported_meanClass_canonical_transport {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → E) (f : ℕ → ℝ × E → V) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hclass : WeightedClasses.MeanClass (logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) : have g := fun (n : ℕ) => TransportPrimitive.compactIntegral (TransportPrimitive.interiorCutoff a b) (M n) (v n) (f n); (∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) ∧ (∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) ∧ WeightedClasses.MeanClass (logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α g

The full supported-mean conclusion includes global smoothness and the original radial support, as required by the smooth zero-extension convention.

noncomputable def NavierStokes.RadialPullback.positiveRadius (ℓ x : ℝ) : ℝ

A globally smooth positive radius, identical to the radius above 2ℓ.

Equations

• NavierStokes.RadialPullback.positiveRadius ℓ x = ℓ + (x - ℓ) * ((x - ℓ) / ℓ).smoothTransition

theorem NavierStokes.RadialPullback.positiveRadius_contDiff (ℓ : ℝ) : ContDiff ℝ (↑⊤) (positiveRadius ℓ)

theorem NavierStokes.RadialPullback.positiveRadius_eq_left {ℓ x : ℝ} (hℓ : 0 < ℓ) (hx : x ≤ ℓ) : positiveRadius ℓ x = ℓ

theorem NavierStokes.RadialPullback.positiveRadius_eq_self {ℓ x : ℝ} (hℓ : 0 < ℓ) (hx : 2 * ℓ ≤ x) : positiveRadius ℓ x = x

theorem NavierStokes.RadialPullback.positiveRadius_pos {ℓ : ℝ} (hℓ : 0 < ℓ) (x : ℝ) : 0 < positiveRadius ℓ x

theorem NavierStokes.RadialPullback.positiveRadius_le_max {ℓ : ℝ} (hℓ : 0 < ℓ) (x : ℝ) : positiveRadius ℓ x ≤ max ℓ x

theorem NavierStokes.RadialPullback.positiveRadius_lt {ℓ x t : ℝ} (hℓ : 0 < ℓ) (hℓt : ℓ < t) (hxt : x < t) : positiveRadius ℓ x < t

noncomputable def NavierStokes.RadialPullback.powerChart (d a R : ℝ) : ℝ

Power chart, given by (positiveRadius (a / 4) R) ^ d.

Equations

• NavierStokes.RadialPullback.powerChart d a R = NavierStokes.RadialPullback.positiveRadius (a / 4) R ^ d

noncomputable def NavierStokes.RadialPullback.inverseChart (d a U : ℝ) : ℝ

Inverse chart, given by (positiveRadius (a ^ d / 4) U) ^ d⁻¹.

Equations

• NavierStokes.RadialPullback.inverseChart d a U = NavierStokes.RadialPullback.positiveRadius (a ^ d / 4) U ^ d⁻¹

noncomputable def NavierStokes.RadialPullback.radialJacobian (d R : ℝ) : ℝ

Radial jacobian, given by d * R ^ (d - 1).

Equations

• NavierStokes.RadialPullback.radialJacobian d R = d * R ^ (d - 1)

theorem NavierStokes.RadialPullback.powerChart_contDiff {a : ℝ} (ha : 0 < a) (d : ℝ) : ContDiff ℝ (↑⊤) (powerChart d a)

theorem NavierStokes.RadialPullback.inverseChart_contDiff {a : ℝ} (ha : 0 < a) (d : ℝ) : ContDiff ℝ (↑⊤) (inverseChart d a)

theorem NavierStokes.RadialPullback.powerChart_pos {a : ℝ} (ha : 0 < a) (d R : ℝ) : 0 < powerChart d a R

theorem NavierStokes.RadialPullback.inverseChart_pos {a : ℝ} (ha : 0 < a) (d U : ℝ) : 0 < inverseChart d a U

theorem NavierStokes.RadialPullback.radialJacobian_pos {d R : ℝ} (hd : 0 < d) (hR : 0 < R) : 0 < radialJacobian d R

theorem NavierStokes.RadialPullback.powerChart_eq {a R : ℝ} (ha : 0 < a) (hR : a / 2 ≤ R) (d : ℝ) : powerChart d a R = R ^ d

theorem NavierStokes.RadialPullback.inverseChart_eq {a U : ℝ} (ha : 0 < a) (d : ℝ) (hU : a ^ d / 2 ≤ U) : inverseChart d a U = U ^ d⁻¹

theorem NavierStokes.RadialPullback.inverseChart_power {a R d : ℝ} (ha : 0 < a) (hd : 0 < d) (hR : a ≤ R) : inverseChart d a (R ^ d) = R

theorem NavierStokes.RadialPullback.powerChart_inverse {a U d : ℝ} (ha : 0 < a) (hd : 0 < d) (hU : a ^ d ≤ U) : powerChart d a (inverseChart d a U) = U

theorem NavierStokes.RadialPullback.inverseChart_rpow {a U d : ℝ} (ha : 0 < a) (hd : 0 < d) (hU : a ^ d ≤ U) : inverseChart d a U ^ d = U

theorem NavierStokes.RadialPullback.powerChart_lt_left {a R d : ℝ} (ha : 0 < a) (hd : 0 < d) (hR : R < a) : powerChart d a R < a ^ d

theorem NavierStokes.RadialPullback.inverseChart_lt_left {a U d : ℝ} (ha : 0 < a) (hd : 0 < d) (hU : U < a ^ d) : inverseChart d a U < a

theorem NavierStokes.RadialPullback.powerChart_gt_right {a b R d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hR : b < R) : b ^ d < powerChart d a R

theorem NavierStokes.RadialPullback.inverseChart_gt_right {a b U d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hU : b ^ d < U) : b < inverseChart d a U

theorem NavierStokes.RadialPullback.powerChart_mem {a b R d : ℝ} (ha : 0 < a) (hd : 0 < d) (hR : R ∈ Set.Ioo a b) : powerChart d a R ∈ Set.Ioo (a ^ d) (b ^ d)

theorem NavierStokes.RadialPullback.inverseChart_mem {a b U d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hU : U ∈ Set.Ioo (a ^ d) (b ^ d)) : inverseChart d a U ∈ Set.Ioo a b

theorem NavierStokes.RadialPullback.powerChart_hasDerivAt {a R : ℝ} (ha : 0 < a) (hR : a / 2 < R) (d : ℝ) : HasDerivAt (powerChart d a) (radialJacobian d R) R

noncomputable def NavierStokes.RadialPullback.liftChart {E : Type} (φ : ℝ → ℝ) (z : ℝ × E) : ℝ × E

Lift chart, given by (φ z.1, z.2).

Equations

• NavierStokes.RadialPullback.liftChart φ z = (φ z.1, z.2)

theorem NavierStokes.RadialPullback.liftChart_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (liftChart φ)

theorem NavierStokes.RadialPullback.liftChart_hasFDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {c : ℝ} (z : ℝ × E) (hφ : HasDerivAt φ c z.1) : HasFDerivAt (liftChart φ) ((c • ContinuousLinearMap.fst ℝ ℝ E).prod (ContinuousLinearMap.snd ℝ ℝ E)) z

noncomputable def NavierStokes.RadialPullback.sourceMultiplier (d a U : ℝ) : ℝ

Source multiplier, given by (radialJacobian d (inverseChart d a U))⁻¹.

Equations

• NavierStokes.RadialPullback.sourceMultiplier d a U = (NavierStokes.RadialPullback.radialJacobian d (NavierStokes.RadialPullback.inverseChart d a U))⁻¹

noncomputable def NavierStokes.RadialPullback.normalizeSource {E V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (d a : ℝ) (g : ℝ × E → V) (z : ℝ × E) : V

Normalize source, given by sourceMultiplier d a z.1 • g (liftChart (inverseChart d a) z).

Equations

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

theorem NavierStokes.RadialPullback.sourceMultiplier_contDiff {a d : ℝ} (ha : 0 < a) (hd : 0 < d) : ContDiff ℝ (↑⊤) (sourceMultiplier d a)

theorem NavierStokes.RadialPullback.normalizeSource_contDiff {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a d : ℝ} (ha : 0 < a) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (normalizeSource d a g)

theorem NavierStokes.RadialPullback.normalizeSource_at_power {E V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a R d : ℝ} (ha : 0 < a) (hd : 0 < d) (hR : a ≤ R) (g : ℝ × E → V) (Y : E) : normalizeSource d a g (R ^ d, Y) = (radialJacobian d R)⁻¹ • g (R, Y)

theorem NavierStokes.RadialPullback.normalizeSource_supported {E V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hs : RadialAlias.RadiallySupported a b g) : RadialAlias.RadiallySupported (a ^ d) (b ^ d) (normalizeSource d a g)

theorem NavierStokes.RadialPullback.normalizeSource_eq_formula {E V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d U : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hU : 0 < U) {g : ℝ × E → V} (hs : RadialAlias.RadiallySupported a b g) (Y : E) : normalizeSource d a g (U, Y) = (radialJacobian d (U ^ d⁻¹))⁻¹ • g (U ^ d⁻¹, Y)

noncomputable def NavierStokes.RadialPullback.pullback {E V : Type} (d a : ℝ) (F : ℝ × E → V) : ℝ × E → V

Pullback, given by F ∘ liftChart (powerChart d a).

Equations

• NavierStokes.RadialPullback.pullback d a F = F ∘ NavierStokes.RadialPullback.liftChart (NavierStokes.RadialPullback.powerChart d a)

theorem NavierStokes.RadialPullback.pullback_contDiff {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} (ha : 0 < a) (d : ℝ) {F : ℝ × E → V} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (pullback d a F)

theorem NavierStokes.RadialPullback.pullback_supported {E V : Type} [NormedAddCommGroup V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {F : ℝ × E → V} (hs : RadialAlias.RadiallySupported (a ^ d) (b ^ d) F) : RadialAlias.RadiallySupported a b (pullback d a F)

noncomputable def NavierStokes.RadialPullback.physicalGraphDeriv {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (d M : ℝ) (v : E) (F : ℝ × E → V) (z : ℝ × E) : V

Physical graph derivative, given by fderiv ℝ F z (1, (radialJacobian d z.1 * M) • v).

Equations

• NavierStokes.RadialPullback.physicalGraphDeriv d M v F z = (fderiv ℝ F z) (1, (NavierStokes.RadialPullback.radialJacobian d z.1 * M) • v)

theorem NavierStokes.RadialPullback.physicalGraphDeriv_pullback {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a d M : ℝ} (ha : 0 < a) (v : E) {F : ℝ × E → V} (z : ℝ × E) (hz : a / 2 < z.1) (hF : DifferentiableAt ℝ F (liftChart (powerChart d a) z)) : physicalGraphDeriv d M v (pullback d a F) z = radialJacobian d z.1 • TransportPrimitive.fixedDeriv (1, M • v) F (liftChart (powerChart d a) z)

The physical radial graph derivative is the transformed transport derivative multiplied by the actual power-coordinate Jacobian.

theorem NavierStokes.RadialPullback.auxiliaryDeriv_pullback {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a d : ℝ} (ha : 0 < a) (w : E) {F : ℝ × E → V} (z : ℝ × E) (hz : a / 2 < z.1) (hF : DifferentiableAt ℝ F (liftChart (powerChart d a) z)) : TransportPrimitive.fixedDeriv (0, w) (pullback d a F) z = TransportPrimitive.fixedDeriv (0, w) F (liftChart (powerChart d a) z)

Pure auxiliary derivatives are unchanged by the radial coordinate map.

theorem NavierStokes.RadialPullback.power_substitution {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a R d : ℝ} (ha : 0 < a) (hR : a ≤ R) (F : ℝ → V) (hF : Continuous F) : ∫ (s : ℝ) in a..R, radialJacobian d s • F (s ^ d) = ∫ (U : ℝ) in a ^ d..R ^ d, F U

The positive power substitution includes the actual radial Jacobian.

theorem NavierStokes.RadialPullback.normalized_radial_integral {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a R d : ℝ} (ha : 0 < a) (hd : 0 < d) (hR : a ≤ R) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (M U₀ : ℝ) (v Y : E) : ∫ (U : ℝ) in a ^ d..R ^ d, normalizeSource d a g (U, Y + (M * (U - U₀)) • v) = ∫ (s : ℝ) in a..R, g (s, Y + (M * (s ^ d - U₀)) • v)

After source normalization, the Jacobian cancels exactly, including the auxiliary shift in the transformed coordinate.

theorem NavierStokes.RadialPullback.total_normalized_eq_radialIntegral {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (M U : ℝ) (v Y : E) : TransportPrimitive.totalIntegral M v (normalizeSource d a g) (U, Y) = ∫ (s : ℝ) in a..b, g (s, Y + (M * (s ^ d - U)) • v)

The total transformed integral has exactly the original physical radial measure. In particular no Jacobian remains when taking a torus mean later.

noncomputable def NavierStokes.RadialPullback.physicalCompact {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (d a b M : ℝ) (v : E) (g : ℝ × E → V) : ℝ × E → V

Physical compact, given by pullback d a (TransportPrimitive.compactIntegral (TransportPrimitive.interiorCutoff (a ^ d) (b ^ d)) M v (normalizeSource d a g)).

Equations

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

theorem NavierStokes.RadialPullback.physicalCompact_contDiff {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : E) : ContDiff ℝ (↑⊤) (physicalCompact d a b M v g)

theorem NavierStokes.RadialPullback.physicalCompact_supported {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : E) : RadialAlias.RadiallySupported a b (physicalCompact d a b M v g)

theorem NavierStokes.RadialPullback.physicalCompact_eq_radialIntegral {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : E) (z : ℝ × E) (hz : a ≤ z.1) : physicalCompact d a b M v g z = (∫ (s : ℝ) in a..z.1, g (s, z.2 + (M * (s ^ d - z.1 ^ d)) • v)) - TransportPrimitive.interiorCutoff (a ^ d) (b ^ d) (z.1 ^ d) • ∫ (s : ℝ) in a..b, g (s, z.2 + (M * (s ^ d - z.1 ^ d)) • v)

The pulled-back operator is the physical shifted radial integral, with the original source g and no uncancelled Jacobian.

noncomputable def NavierStokes.RadialPullback.physicalAlias {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (d a b M : ℝ) (v : E) (g : ℝ × E → V) (z : ℝ × E) : V

Physical alias as an element of V.

Equations

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

noncomputable def NavierStokes.RadialPullback.physicalCutoff (d a b R : ℝ) : ℝ

Physical cutoff, given by TransportPrimitive.interiorCutoff (a ^ d) (b ^ d) (powerChart d a R).

Equations

• NavierStokes.RadialPullback.physicalCutoff d a b R = NavierStokes.TransportPrimitive.interiorCutoff (a ^ d) (b ^ d) (NavierStokes.RadialPullback.powerChart d a R)

theorem NavierStokes.RadialPullback.physicalCutoff_contDiff {a : ℝ} (ha : 0 < a) (d b : ℝ) : ContDiff ℝ (↑⊤) (physicalCutoff d a b)

theorem NavierStokes.RadialPullback.deriv_physicalCutoff {a R : ℝ} (ha : 0 < a) (hR : a / 2 < R) (d b : ℝ) : deriv (physicalCutoff d a b) R = radialJacobian d R * deriv (TransportPrimitive.interiorCutoff (a ^ d) (b ^ d)) (powerChart d a R)

theorem NavierStokes.RadialPullback.physicalAlias_eq_cutoff_derivative {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a d b M : ℝ} (ha : 0 < a) (v : E) (g : ℝ × E → V) (z : ℝ × E) (hz : a / 2 < z.1) : physicalAlias d a b M v g z = deriv (physicalCutoff d a b) z.1 • TransportPrimitive.totalIntegral M v (normalizeSource d a g) (liftChart (powerChart d a) z)

theorem NavierStokes.RadialPullback.physicalGraphDeriv_physicalCompact {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : E) (z : ℝ × E) (hz : a ≤ z.1) : physicalGraphDeriv d M v (physicalCompact d a b M v g) z = g z - physicalAlias d a b M v g z

Exact inverse identity in the physical radial graph coordinate, including the compactification alias and the source normalization.

theorem NavierStokes.RadialPullback.deriv_interiorCutoff_zero_left {a b U : ℝ} (hab : a < b) (hU : U ≤ a) : deriv (TransportPrimitive.interiorCutoff a b) U = 0

theorem NavierStokes.RadialPullback.deriv_interiorCutoff_zero_right {a b U : ℝ} (hab : a < b) (hU : b ≤ U) : deriv (TransportPrimitive.interiorCutoff a b) U = 0

theorem NavierStokes.RadialPullback.physicalAlias_supported {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : E) (g : ℝ × E → V) : RadialAlias.RadiallySupported a b (physicalAlias d a b M v g)

theorem NavierStokes.RadialPullback.physicalCutoff_zero_left {a b d R : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hR : R < a) : physicalCutoff d a b R = 0

theorem NavierStokes.RadialPullback.deriv_physicalCutoff_zero_left {a b d R : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hR : R < a) : deriv (physicalCutoff d a b) R = 0

theorem NavierStokes.RadialPullback.physicalAlias_eq_cutoff_derivative_global {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) (g : ℝ × E → V) (z : ℝ × E) : physicalAlias d a b M v g z = deriv (physicalCutoff d a b) z.1 • TransportPrimitive.totalIntegral M v (normalizeSource d a g) (liftChart (powerChart d a) z)

theorem NavierStokes.RadialPullback.physicalAlias_contDiff {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : E) : ContDiff ℝ (↑⊤) (physicalAlias d a b M v g)

theorem NavierStokes.RadialPullback.physicalGraphDeriv_physicalCompact_global {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {a b d : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) {g : ℝ × E → V} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (M : ℝ) (v : E) (z : ℝ × E) : physicalGraphDeriv d M v (physicalCompact d a b M v g) z = g z - physicalAlias d a b M v g z

Global physical inverse identity. Below the positive annulus, the source, the output derivative, and the alias all vanish by their proved support.

Exact exponential weight and controlled inverse-edge powers

theorem NavierStokes.RadialPullback.logPosition_power {a R : ℝ} (ha : 0 < a) (hR : 0 < R) (d : ℝ) : WeightedRadialPrimitive.logPosition (a ^ d) (R ^ d) = d * WeightedRadialPrimitive.logPosition a R

theorem NavierStokes.RadialPullback.logLength_power {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (d : ℝ) : WeightedRadialPrimitive.logLength (a ^ d) (b ^ d) = d * WeightedRadialPrimitive.logLength a b

theorem NavierStokes.RadialPullback.delta_scale_lower {d L x : ℝ} (hd : 0 < d) (hx : x ∈ Set.Ioo 0 L) : min 1 d * WeightedRadialPrimitive.delta L x ≤ WeightedRadialPrimitive.delta (d * L) (d * x)

theorem NavierStokes.RadialPullback.delta_scale_reverse_lower {d L x : ℝ} (hd : 0 < d) (hx : x ∈ Set.Ioo 0 L) : min 1 d⁻¹ * WeightedRadialPrimitive.delta (d * L) (d * x) ≤ WeightedRadialPrimitive.delta L x

theorem NavierStokes.RadialPullback.edge_scaled (c : ℝ) {d x : ℝ} (hd : 0 < d) (hx : 0 < x) : FlatCutoff.edge (d ^ 2 * c) (d * x) = FlatCutoff.edge c x

theorem NavierStokes.RadialPullback.zeta_scaled (cL cR : ℝ) {d L x : ℝ} (hd : 0 < d) (hx : x ∈ Set.Ioo 0 L) : WeightedRadialPrimitive.zeta (d ^ 2 * cL) (d ^ 2 * cR) (d * L) (d * x) = WeightedRadialPrimitive.zeta cL cR L x

theorem NavierStokes.RadialPullback.weight_scale_forward (cL cR : ℝ) {d L x : ℝ} (hd : 0 < d) (hx : x ∈ Set.Ioo 0 L) (p : ℕ) : WeightedRadialPrimitive.weight (d ^ 2 * cL) (d ^ 2 * cR) (d * L) p (d * x) ≤ (min 1 d ^ p)⁻¹ * WeightedRadialPrimitive.weight cL cR L p x

theorem NavierStokes.RadialPullback.weight_scale_reverse (cL cR : ℝ) {d L x : ℝ} (hd : 0 < d) (hx : x ∈ Set.Ioo 0 L) (p : ℕ) : WeightedRadialPrimitive.weight cL cR L p x ≤ (min 1 d⁻¹ ^ p)⁻¹ * WeightedRadialPrimitive.weight (d ^ 2 * cL) (d ^ 2 * cR) (d * L) p (d * x)

theorem NavierStokes.RadialPullback.logWeight_power_forward {a b R d : ℝ} (ha : 0 < a) (hd : 0 < d) (hR : R ∈ Set.Ioo a b) (cL cR : ℝ) (p : ℕ) : WeightedRadialPrimitive.logWeight (d ^ 2 * cL) (d ^ 2 * cR) (a ^ d) (b ^ d) p (R ^ d) ≤ (min 1 d ^ p)⁻¹ * WeightedRadialPrimitive.logWeight cL cR a b p R

Scaling the exponential coefficients by d² preserves exactly the same exponential flat weight under U=R^d; only a fixed clipped-edge factor changes.

theorem NavierStokes.RadialPullback.logWeight_power_reverse {a b R d : ℝ} (ha : 0 < a) (hd : 0 < d) (hR : R ∈ Set.Ioo a b) (cL cR : ℝ) (p : ℕ) : WeightedRadialPrimitive.logWeight cL cR a b p R ≤ (min 1 d⁻¹ ^ p)⁻¹ * WeightedRadialPrimitive.logWeight (d ^ 2 * cL) (d ^ 2 * cR) (a ^ d) (b ^ d) p (R ^ d)

Uniform genuine finite jets under fixed radial maps

theorem NavierStokes.RadialPullback.liftChart_jet_aux_independent {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (n : ℕ) (R : ℝ) (Y : E) : iteratedFDeriv ℝ (n + 1) (liftChart φ) (R, Y) = iteratedFDeriv ℝ (n + 1) (liftChart φ) (R, 0)

Positive-order derivatives of a radial coordinate change are independent of the auxiliary base point. This follows from translation identities.

theorem NavierStokes.RadialPullback.liftChart_positive_jets_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (j : ℕ), 1 ≤ j → j ≤ m → ∀ (z : ℝ × E), z.1 ∈ Set.Icc a b → ‖iteratedFDeriv ℝ j (liftChart φ) z‖ ≤ B

theorem NavierStokes.RadialPullback.radial_comp_finiteJets_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (a b : ℝ) {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (F : ℝ × E → V), ContDiff ℝ (↑⊤) F → ∀ (z : ℝ × E), z.1 ∈ Set.Icc a b → ∀ (C : ℝ), 0 ≤ C → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (liftChart φ z)‖ ≤ C) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (F ∘ liftChart φ) z‖ ≤ K * C

A fixed radial coordinate map has a finite-order composition constant, uniform on the full auxiliary strip, for actual multilinear derivative norms.

theorem NavierStokes.RadialPullback.radial_multiplier_finiteJets_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (a b : ℝ) {h : ℝ → ℝ} (hh : ContDiff ℝ (↑⊤) h) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (F : ℝ × E → V), ContDiff ℝ (↑⊤) F → ∀ (z : ℝ × E), z.1 ∈ Set.Icc a b → ∀ (C : ℝ), 0 ≤ C → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F z‖ ≤ C) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (fun (y : ℝ × E) => h y.1 • F y) z‖ ≤ K * C

Multiplication by a fixed smooth radial coefficient has a finite-order constant, with all product-rule terms retained.

Weighted source normalization

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

theorem NavierStokes.RadialPullback.physicalCompact_finiteJets_uniform {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [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 : E) (g : ℝ × E → V), ContDiff ℝ (↑⊤) g → RadialAlias.RadiallySupported a b g → ∀ (A : ℝ), 0 ≤ A → (∀ j ≤ m, ∀ R ∈ Set.Ioo a b, ∀ (Y : E), ‖iteratedFDeriv ℝ j g (R, Y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR a b p R) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo a b → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (physicalCompact d a b M 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.

theorem NavierStokes.RadialPullback.meanClass_physicalCompact {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [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) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → E) (g : ℕ → ℝ × E → V) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α g) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α fun (n : ℕ) => physicalCompact d a b (M n) (v n) (g n)

The physical/chart inverse maps the concrete all-jet mean class to itself. The input and output weights are exactly the same logarithmic exponential.

theorem NavierStokes.RadialPullback.supported_meanClass_physicalCompact {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [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) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (α : ℝ) (M : ℕ → ℝ) (v : ℕ → E) (g : ℕ → ℝ × E → V) (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (g n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α g) : have F := fun (n : ℕ) => physicalCompact d a b (M n) (v n) (g n); (∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) ∧ (∀ (n : ℕ), RadialAlias.RadiallySupported a b (F n)) ∧ WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α F