Homogeneity of the actual similarity coordinates

The coordinate q is the positive branch constructed in SimilarityCoordinates. Its scaling law follows from uniqueness of that branch. The band coordinates below are (R,(Z,T)), with T = τ / Q. Consequently the profile coordinate is X = R² / (2 q(T,Z)), not a fixed function of R alone. Profile weights are transported exactly by a change of band scale.

@[reducible, inline]

noncomputable abbrev NavierStokes.SimilarityHomogeneity.D (h : ℝ) : ℝ

D: an abbreviation for CoordinateAlgebra.D.

Equations

• NavierStokes.SimilarityHomogeneity.D = NavierStokes.CoordinateAlgebra.D

theorem NavierStokes.SimilarityHomogeneity.forwardScalar_scale {Q q : ℝ} (hQ : 0 < Q) (hq : 0 < q) (a z : ℝ) : SimilarityCoordinates.forwardScalar a (Q ^ ((1 - a) / 2) * z) (Q * q) = Q * SimilarityCoordinates.forwardScalar a z q

The scalar defining equation has the required anisotropic homogeneity.

theorem NavierStokes.SimilarityHomogeneity.coordinateQ_scale {a Q τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hQ : 0 < Q) (hτ : 0 < τ) : SimilarityCoordinates.coordinateQ a (Q * τ, Q ^ ((1 - a) / 2) * z) = Q * SimilarityCoordinates.coordinateQ a (τ, z)

Exact scaling of the defined coordinate, obtained by positive-branch uniqueness rather than by postulating homogeneity.

theorem NavierStokes.SimilarityHomogeneity.coordinateEta_scale {a Q τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hQ : 0 < Q) (hτ : 0 < τ) : SimilarityCoordinates.coordinateEta a (Q * τ, Q ^ ((1 - a) / 2) * z) = SimilarityCoordinates.coordinateEta a (τ, z)

The defined axial similarity parameter is invariant under scaling.

theorem NavierStokes.SimilarityHomogeneity.coordinateX_scale {a Q τ z s : ℝ} (ha : 0 < a) (ha1 : a < 1) (hQ : 0 < Q) (hτ : 0 < τ) : SimilarityCoordinates.coordinateX a (Q * s) (Q * τ, Q ^ ((1 - a) / 2) * z) = SimilarityCoordinates.coordinateX a s (τ, z)

Scaling s and τ by the same factor preserves the defined X.

theorem NavierStokes.SimilarityHomogeneity.coordinateQ_scale_h {h Q τ z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hτ : 0 < τ) : SimilarityCoordinates.coordinateQ (2 * h) (Q * τ, Q ^ D h * z) = Q * SimilarityCoordinates.coordinateQ (2 * h) (τ, z)

The manuscript's exact h,D convention.

theorem NavierStokes.SimilarityHomogeneity.coordinateEta_scale_h {h Q τ z : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hτ : 0 < τ) : SimilarityCoordinates.coordinateEta (2 * h) (Q * τ, Q ^ D h * z) = SimilarityCoordinates.coordinateEta (2 * h) (τ, z)

theorem NavierStokes.SimilarityHomogeneity.coordinateX_scale_h {h Q τ z s : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hτ : 0 < τ) : SimilarityCoordinates.coordinateX (2 * h) (Q * s) (Q * τ, Q ^ D h * z) = SimilarityCoordinates.coordinateX (2 * h) s (τ, z)

noncomputable def NavierStokes.SimilarityHomogeneity.physicalScale (h Q : ℝ) (p : SimilarityProfile.PhysicalPoint) : SimilarityProfile.PhysicalPoint

Physical time is t=1-τ; physical points have layout (t,(s,z)).

Equations

• NavierStokes.SimilarityHomogeneity.physicalScale h Q p = (1 - Q * (1 - p.1), Q * p.2.1, Q ^ NavierStokes.SimilarityHomogeneity.D h * p.2.2)

theorem NavierStokes.SimilarityHomogeneity.physicalScale_smooth (h Q : ℝ) : ContDiff ℝ (↑⊤) (physicalScale h Q)

theorem NavierStokes.SimilarityHomogeneity.physicalScale_time_lt_one {h Q : ℝ} (hQ : 0 < Q) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : (physicalScale h Q p).1 < 1

theorem NavierStokes.SimilarityHomogeneity.q_physicalScale {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : SimilarityProfile.q h (physicalScale h Q p) = Q * SimilarityProfile.q h p

theorem NavierStokes.SimilarityHomogeneity.eta_physicalScale {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : SimilarityProfile.eta h (physicalScale h Q p) = SimilarityProfile.eta h p

theorem NavierStokes.SimilarityHomogeneity.X_physicalScale {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : SimilarityProfile.X h (physicalScale h Q p) = SimilarityProfile.X h p

theorem NavierStokes.SimilarityHomogeneity.inner_physicalScale {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : SimilarityProfile.inner h (physicalScale h Q p) = SimilarityProfile.inner h p

theorem NavierStokes.SimilarityHomogeneity.pullback_physicalScale {h Q b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (f : SimilarityProfile.InnerProfile) : SimilarityProfile.pullback h b f (physicalScale h Q p) = Q ^ b * SimilarityProfile.pullback h b f p

Homogeneity holds for every profile, without assuming its smoothness.

@[reducible, inline]

abbrev NavierStokes.SimilarityHomogeneity.ChartPoint : Type

Chart point: an abbreviation for ℝ × (ℝ × ℝ).

Equations

• NavierStokes.SimilarityHomogeneity.ChartPoint = (ℝ × ℝ × ℝ)

noncomputable def NavierStokes.SimilarityHomogeneity.chartQ (h : ℝ) (p : ChartPoint) : ℝ

A band chart is ordered (R,(Z,T)).

Equations

• NavierStokes.SimilarityHomogeneity.chartQ h p = NavierStokes.SimilarityCoordinates.coordinateQ (2 * h) (p.2.2, p.2.1)

noncomputable def NavierStokes.SimilarityHomogeneity.chartEta (h : ℝ) (p : ChartPoint) : ℝ

Chart eta, given by coordinateEta (2 * h) (p.2.2, p.2.1).

Equations

• NavierStokes.SimilarityHomogeneity.chartEta h p = NavierStokes.SimilarityCoordinates.coordinateEta (2 * h) (p.2.2, p.2.1)

noncomputable def NavierStokes.SimilarityHomogeneity.chartX (h : ℝ) (p : ChartPoint) : ℝ

Chart X, given by coordinateX (2 * h) (p.1 ^ 2 / 2) (p.2.2, p.2.1).

Equations

• NavierStokes.SimilarityHomogeneity.chartX h p = NavierStokes.SimilarityCoordinates.coordinateX (2 * h) (p.1 ^ 2 / 2) (p.2.2, p.2.1)

noncomputable def NavierStokes.SimilarityHomogeneity.chartInner (h : ℝ) (p : ChartPoint) : ℝ × ℝ

Chart inner, given by (chartX h p, chartEta h p).

Equations

• NavierStokes.SimilarityHomogeneity.chartInner h p = (NavierStokes.SimilarityHomogeneity.chartX h p, NavierStokes.SimilarityHomogeneity.chartEta h p)

noncomputable def NavierStokes.SimilarityHomogeneity.chartTransition (h Q Q' : ℝ) (p : ChartPoint) : ChartPoint

Transition from the band of scale Q to the band of scale Q'.

Equations

• NavierStokes.SimilarityHomogeneity.chartTransition h Q Q' p = ((Q / Q') ^ (1 / 2) * p.1, (Q / Q') ^ NavierStokes.SimilarityHomogeneity.D h * p.2.1, Q / Q' * p.2.2)

theorem NavierStokes.SimilarityHomogeneity.chartTransition_smooth (h Q Q' : ℝ) : ContDiff ℝ (↑⊤) (chartTransition h Q Q')

theorem NavierStokes.SimilarityHomogeneity.chartTransition_time_pos {h Q Q' : ℝ} (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) : 0 < (chartTransition h Q Q' p).2.2

theorem NavierStokes.SimilarityHomogeneity.chartQ_transition {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) : chartQ h (chartTransition h Q Q' p) = Q / Q' * chartQ h p

theorem NavierStokes.SimilarityHomogeneity.chartEta_transition {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) : chartEta h (chartTransition h Q Q' p) = chartEta h p

theorem NavierStokes.SimilarityHomogeneity.chartX_transition {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) : chartX h (chartTransition h Q Q' p) = chartX h p

theorem NavierStokes.SimilarityHomogeneity.chartInner_transition {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) : chartInner h (chartTransition h Q Q' p) = chartInner h p

noncomputable def NavierStokes.SimilarityHomogeneity.chartToPhysical (h Q : ℝ) (p : ChartPoint) : SimilarityProfile.PhysicalPoint

The genuine chart-to-physical map, with radial variable s=r²/2.

Equations

• NavierStokes.SimilarityHomogeneity.chartToPhysical h Q p = (1 - Q * p.2.2, Q * (p.1 ^ 2 / 2), Q ^ NavierStokes.SimilarityHomogeneity.D h * p.2.1)

theorem NavierStokes.SimilarityHomogeneity.chartToPhysical_smooth (h Q : ℝ) : ContDiff ℝ (↑⊤) (chartToPhysical h Q)

theorem NavierStokes.SimilarityHomogeneity.chartToPhysical_time_lt_one {h Q : ℝ} (hQ : 0 < Q) {p : ChartPoint} (hp : 0 < p.2.2) : (chartToPhysical h Q p).1 < 1

theorem NavierStokes.SimilarityHomogeneity.chartToPhysical_radial {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (p : ChartPoint) : (chartToPhysical h Q p).2.1 = (Scaling.radialLength Q * p.1) ^ 2 / 2

The radial component really is obtained from r = sqrt(Q) R.

theorem NavierStokes.SimilarityHomogeneity.q_chartToPhysical {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : ChartPoint} (hp : 0 < p.2.2) : SimilarityProfile.q h (chartToPhysical h Q p) = Q * chartQ h p

theorem NavierStokes.SimilarityHomogeneity.eta_chartToPhysical {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : ChartPoint} (hp : 0 < p.2.2) : SimilarityProfile.eta h (chartToPhysical h Q p) = chartEta h p

theorem NavierStokes.SimilarityHomogeneity.X_chartToPhysical {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : ChartPoint} (hp : 0 < p.2.2) : SimilarityProfile.X h (chartToPhysical h Q p) = chartX h p

theorem NavierStokes.SimilarityHomogeneity.inner_chartToPhysical {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {p : ChartPoint} (hp : 0 < p.2.2) : SimilarityProfile.inner h (chartToPhysical h Q p) = chartInner h p

theorem NavierStokes.SimilarityHomogeneity.chartToPhysical_transition {h Q Q' : ℝ} (hQ : 0 < Q) (hQ' : 0 < Q') (p : ChartPoint) : chartToPhysical h Q' (chartTransition h Q Q' p) = chartToPhysical h Q p

Two band descriptions of the same physical point agree exactly.

theorem NavierStokes.SimilarityHomogeneity.chartTransition_refl {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (p : ChartPoint) : chartTransition h Q Q p = p

theorem NavierStokes.SimilarityHomogeneity.chartTransition_comp {h Q Q' Q'' : ℝ} (hQ : 0 < Q) (hQ' : 0 < Q') (hQ'' : 0 < Q'') (p : ChartPoint) : chartTransition h Q' Q'' (chartTransition h Q Q' p) = chartTransition h Q Q'' p

theorem NavierStokes.SimilarityHomogeneity.chartTransition_inverse {h Q Q' : ℝ} (hQ : 0 < Q) (hQ' : 0 < Q') (p : ChartPoint) : chartTransition h Q' Q (chartTransition h Q Q' p) = p

noncomputable def NavierStokes.SimilarityHomogeneity.chartDomain : Set ChartPoint

The usual open annular-chart domain; profile annulus restrictions can be added using chartX_mem_transition.

Equations

• NavierStokes.SimilarityHomogeneity.chartDomain = {p : NavierStokes.SimilarityHomogeneity.ChartPoint | 0 < p.1 ∧ 0 < p.2.2}

theorem NavierStokes.SimilarityHomogeneity.isOpen_chartDomain : IsOpen chartDomain

theorem NavierStokes.SimilarityHomogeneity.chartTransition_mem_iff {h Q Q' : ℝ} (hQ : 0 < Q) (hQ' : 0 < Q') (p : ChartPoint) : chartTransition h Q Q' p ∈ chartDomain ↔ p ∈ chartDomain

theorem NavierStokes.SimilarityHomogeneity.chartInner_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : ChartPoint} (hp : 0 < p.2.2) : ContDiffAt ℝ (↑⊤) (chartInner h) p

theorem NavierStokes.SimilarityHomogeneity.chartX_mem_transition {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) (I : Set ℝ) : chartX h (chartTransition h Q Q' p) ∈ I ↔ chartX h p ∈ I

theorem NavierStokes.SimilarityHomogeneity.chartProfile_transition {E : Type u_1} {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) (F : ℝ × ℝ → E) : F (chartInner h (chartTransition h Q Q' p)) = F (chartInner h p)

Every profile depending on both actual inner coordinates is unchanged.

noncomputable def NavierStokes.SimilarityHomogeneity.chartWeight {E : Type u_1} (h : ℝ) (ζ : ℝ → E) (p : ChartPoint) : E

Chart weight, given by ζ (chartX h p).

Equations

• NavierStokes.SimilarityHomogeneity.chartWeight h ζ p = ζ (NavierStokes.SimilarityHomogeneity.chartX h p)

theorem NavierStokes.SimilarityHomogeneity.chartWeight_transition {E : Type u_1} {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) (ζ : ℝ → E) : chartWeight h ζ (chartTransition h Q Q' p) = chartWeight h ζ p

In particular an arbitrarily flat weight is transported with factor one.

noncomputable def NavierStokes.SimilarityHomogeneity.profileLogDistance (left right X : ℝ) : ℝ

The lesser of one and the two logarithmic distances to fixed profile edges. Positivity is asserted only inside a positive profile interval.

Equations

• NavierStokes.SimilarityHomogeneity.profileLogDistance left right X = min 1 (min (Real.log X - Real.log left) (Real.log right - Real.log X))

theorem NavierStokes.SimilarityHomogeneity.profileLogDistance_pos {left right X : ℝ} (hl : 0 < left) (hLX : left < X) (hXR : X < right) : 0 < profileLogDistance left right X

noncomputable def NavierStokes.SimilarityHomogeneity.chartLogDistance (h left right : ℝ) (p : ChartPoint) : ℝ

Chart log distance, given by profileLogDistance left right (chartX h p).

Equations

• NavierStokes.SimilarityHomogeneity.chartLogDistance h left right p = NavierStokes.SimilarityHomogeneity.profileLogDistance left right (NavierStokes.SimilarityHomogeneity.chartX h p)

theorem NavierStokes.SimilarityHomogeneity.chartLogDistance_transition {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) (left right : ℝ) : chartLogDistance h left right (chartTransition h Q Q' p) = chartLogDistance h left right p

theorem NavierStokes.SimilarityHomogeneity.chartWeightedFactor_transition {h Q Q' : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQ' : 0 < Q') {p : ChartPoint} (hp : 0 < p.2.2) (ζ : ℝ → ℝ) (left right exponent : ℝ) : √(chartWeight h ζ (chartTransition h Q Q' p)) * chartLogDistance h left right (chartTransition h Q Q' p) ^ exponent = √(chartWeight h ζ p) * chartLogDistance h left right p ^ exponent

Exact transport includes square-root flat weights and every real edge power, including the negative powers used for derivative losses.