Positive-time representatives and the genuine stable inverse branch

The totalized coordinateQ is used only at positive time. A different, constructed inverse extends the stable branch across its regular zero-time face. The actual mask representatives stay at positive time.

@[reducible, inline]

abbrev NavierStokes.PositiveRepresentatives.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.PositiveRepresentatives.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.PositiveRepresentatives.Label : Type

Label: an abbreviation for PartitionedCovariance.UnsignedLabel.

Equations

• NavierStokes.PositiveRepresentatives.Label = NavierStokes.PartitionedCovariance.UnsignedLabel

noncomputable def NavierStokes.PositiveRepresentatives.positiveTime : Set Slow

Positive time, given by {p | 0 < p.2.2}.

Equations

• NavierStokes.PositiveRepresentatives.positiveTime = {p : NavierStokes.PositiveRepresentatives.Slow | 0 < p.2.2}

noncomputable def NavierStokes.PositiveRepresentatives.positivePart (K : Set Slow) : Set Slow

Positive part, given by K ∩ positiveTime.

Equations

• NavierStokes.PositiveRepresentatives.positivePart K = K ∩ NavierStokes.PositiveRepresentatives.positiveTime

noncomputable def NavierStokes.PositiveRepresentatives.ActiveLabel (K : Set Slow) : Type

Active label, given by PrimaryRepresentatives.ActiveLabel (positivePart K).

Equations

• NavierStokes.PositiveRepresentatives.ActiveLabel K = NavierStokes.PrimaryRepresentatives.ActiveLabel (NavierStokes.PositiveRepresentatives.positivePart K)

noncomputable def NavierStokes.PositiveRepresentatives.representative (K : Set Slow) (L : ActiveLabel K) : Slow

Representative, given by PrimaryRepresentatives.representative (positivePart K) L.

Equations

• NavierStokes.PositiveRepresentatives.representative K L = NavierStokes.PrimaryRepresentatives.representative (NavierStokes.PositiveRepresentatives.positivePart K) L

theorem NavierStokes.PositiveRepresentatives.positiveTime_open : IsOpen positiveTime

theorem NavierStokes.PositiveRepresentatives.positiveTime_convex : Convex ℝ positiveTime

theorem NavierStokes.PositiveRepresentatives.representative_mem (K : Set Slow) (L : ActiveLabel K) : representative K L ∈ K

theorem NavierStokes.PositiveRepresentatives.representative_time_pos (K : Set Slow) (L : ActiveLabel K) : 0 < (representative K L).2.2

theorem NavierStokes.PositiveRepresentatives.representative_mem_tsupport (K : Set Slow) (L : ActiveLabel K) : representative K L ∈ tsupport (PrimaryRepresentatives.nativeMask (↑L).1 (↑L).2)

theorem NavierStokes.PositiveRepresentatives.representative_enlarged_distance (K : Set Slow) (L : ActiveLabel K) {p : Slow} (hp : p ∈ PrimaryRepresentatives.gridBox (↑L).1 (↑L).2 2) : ‖p - representative K L‖ ≤ 3 / ChartScales.S (↑L).1 ^ 3

theorem NavierStokes.PositiveRepresentatives.representative_support_distance (K : Set Slow) (L : ActiveLabel K) {p : Slow} (hp : p ∈ tsupport (PrimaryRepresentatives.nativeMask (↑L).1 (↑L).2)) : ‖p - representative K L‖ ≤ 2 / ChartScales.S (↑L).1 ^ 3

theorem NavierStokes.PositiveRepresentatives.physicalMask_has_positive_representative {h a b : ℝ} (L : Label) (hL : 1 ≤ L.1) {q : ℝ} {x : SlotColoring.Position} (hq : 0 < q) (hR : 0 ≤ x 0) (hT : 0 < x 2) (he : SimilarityCoordinates.forwardScalar (2 * h) (x 1) q = x 2) (hX : x 0 ^ 2 / (2 * q) ∈ Set.Icc a b) (hm : PartitionedCovariance.mask (CoordinateAlgebra.D h) L q x ≠ 0) : ∃ (A : ActiveLabel (PrimaryRepresentatives.referenceCompact h a b)), ↑A = L

A smooth inverse on the stable branch, including its zero-time face

noncomputable def NavierStokes.PositiveRepresentatives.stableSource (a : ℝ) : Set (ℝ × ℝ)

Stable source, given by {p | 0 < p.1 ∧ 0 < scalarSlope a p.2 p.1}.

Equations

• NavierStokes.PositiveRepresentatives.stableSource a = {p : ℝ × ℝ | 0 < p.1 ∧ 0 < NavierStokes.SimilarityCoordinates.scalarSlope a p.2 p.1}

noncomputable def NavierStokes.PositiveRepresentatives.stableTarget (a : ℝ) : Set (ℝ × ℝ)

Stable target, given by forwardMap a '' stableSource a.

Equations

• NavierStokes.PositiveRepresentatives.stableTarget a = NavierStokes.SimilarityCoordinates.forwardMap a '' NavierStokes.PositiveRepresentatives.stableSource a

theorem NavierStokes.PositiveRepresentatives.scalarSlope_smoothAt {a : ℝ} {p : ℝ × ℝ} (hp : p.1 ≠ 0) : ContDiffAt ℝ (↑⊤) (fun (x : ℝ × ℝ) => SimilarityCoordinates.scalarSlope a x.2 x.1) p

theorem NavierStokes.PositiveRepresentatives.stableSource_open (a : ℝ) : IsOpen (stableSource a)

theorem NavierStokes.PositiveRepresentatives.scalarSlope_lower_of_nonnegative {a q z : ℝ} (ha : 0 ≤ a) (hq : 0 < q) (hf : 0 ≤ SimilarityCoordinates.forwardScalar a z q) : 1 - a ≤ SimilarityCoordinates.scalarSlope a z q

theorem NavierStokes.PositiveRepresentatives.scalarSlope_mono {a z q r : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) (hq : 0 < q) (hqr : q ≤ r) : SimilarityCoordinates.scalarSlope a z q ≤ SimilarityCoordinates.scalarSlope a z r

theorem NavierStokes.PositiveRepresentatives.forwardScalar_hasDerivAt {a z q : ℝ} (hq : q ≠ 0) : HasDerivAt (SimilarityCoordinates.forwardScalar a z) (SimilarityCoordinates.scalarSlope a z q) q

theorem NavierStokes.PositiveRepresentatives.forwardScalar_lt_on_stable {a z q r : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) (hq : 0 < q) (hm : 0 < SimilarityCoordinates.scalarSlope a z q) (hqr : q < r) : SimilarityCoordinates.forwardScalar a z q < SimilarityCoordinates.forwardScalar a z r

theorem NavierStokes.PositiveRepresentatives.forwardMap_injOn_stable {a : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) : Set.InjOn (SimilarityCoordinates.forwardMap a) (stableSource a)

noncomputable def NavierStokes.PositiveRepresentatives.stableInverse (a : ℝ) (p : ℝ × ℝ) : ℝ × ℝ

Stable inverse, choosing the witness provided by hp.

Equations

• NavierStokes.PositiveRepresentatives.stableInverse a p = if hp : p ∈ NavierStokes.PositiveRepresentatives.stableTarget a then Classical.choose hp else (1, p.2)

theorem NavierStokes.PositiveRepresentatives.stableInverse_spec {a : ℝ} {p : ℝ × ℝ} (hp : p ∈ stableTarget a) : stableInverse a p ∈ stableSource a ∧ SimilarityCoordinates.forwardMap a (stableInverse a p) = p

theorem NavierStokes.PositiveRepresentatives.stableInverse_forwardMap {a : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) {p : ℝ × ℝ} (hp : p ∈ stableSource a) : stableInverse a (SimilarityCoordinates.forwardMap a p) = p

theorem NavierStokes.PositiveRepresentatives.stableTarget_open (a : ℝ) : IsOpen (stableTarget a)

theorem NavierStokes.PositiveRepresentatives.stableInverse_smoothAt {a : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) {p : ℝ × ℝ} (hp : p ∈ stableTarget a) : ContDiffAt ℝ (↑⊤) (stableInverse a) p

theorem NavierStokes.PositiveRepresentatives.positiveTime_mem_stableTarget {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : p ∈ stableTarget a

theorem NavierStokes.PositiveRepresentatives.stableInverse_eq_inverseMap {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : stableInverse a p = SimilarityCoordinates.inverseMap a p

The old closed reference set lies inside the regular stable target

noncomputable def NavierStokes.PositiveRepresentatives.forwardSlow (h : ℝ) (p : Slow) : Slow

Source coordinates are (R,(Z,rho)), with rho independent of the totalized inverse.

Equations

• NavierStokes.PositiveRepresentatives.forwardSlow h p = (p.1, p.2.1, NavierStokes.SimilarityCoordinates.forwardScalar (2 * h) p.2.1 p.2.2)

noncomputable def NavierStokes.PositiveRepresentatives.liftedBox (a b : ℝ) : Set Slow

Lifted box, given by Icc (Real.sqrt a) (2 * Real.sqrt b) ×ˢ (Icc (-2 : ℝ) 2 ×ˢ Icc (1 / 2 : ℝ) 2).

Equations

• NavierStokes.PositiveRepresentatives.liftedBox a b = Set.Icc (√a) (2 * √b) ×ˢ Set.Icc (-2) 2 ×ˢ Set.Icc (1 / 2) 2

noncomputable def NavierStokes.PositiveRepresentatives.liftedReference (h a b : ℝ) : Set Slow

Lifted reference, given by liftedBox a b ∩ {p | 0 ≤ (forwardSlow h p).2.2 ∧ a * (2 * p.2.2) ≤ p.1 ^ 2 ∧ p.1 ^ 2 ≤ b * (2 * p.2.2)}.

Equations

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

theorem NavierStokes.PositiveRepresentatives.forwardSlow_continuous {h : ℝ} (hh : 0 ≤ h) : Continuous (forwardSlow h)

theorem NavierStokes.PositiveRepresentatives.liftedReference_isCompact {h a b : ℝ} (hh : 0 ≤ h) : IsCompact (liftedReference h a b)

theorem NavierStokes.PositiveRepresentatives.activeReference_subset_lifted_image {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : PrimaryRepresentatives.activeReference h a b ⊆ forwardSlow h '' liftedReference h a b

theorem NavierStokes.PositiveRepresentatives.lifted_image_subset_activeReference {h a b : ℝ} : forwardSlow h '' liftedReference h a b ⊆ PrimaryRepresentatives.activeReference h a b

theorem NavierStokes.PositiveRepresentatives.referenceCompact_eq_lifted_image {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : PrimaryRepresentatives.referenceCompact h a b = forwardSlow h '' liftedReference h a b

theorem NavierStokes.PositiveRepresentatives.referenceCompact_eq_activeReference {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : PrimaryRepresentatives.referenceCompact h a b = PrimaryRepresentatives.activeReference h a b

noncomputable def NavierStokes.PositiveRepresentatives.stableDomain (h : ℝ) : Set Slow

Stable domain, given by {p | 0 < p.1 ∧ (p.2.2, p.2.1) ∈ stableTarget (2 * h)}.

Equations

• NavierStokes.PositiveRepresentatives.stableDomain h = {p : NavierStokes.PositiveRepresentatives.Slow | 0 < p.1 ∧ (p.2.2, p.2.1) ∈ NavierStokes.PositiveRepresentatives.stableTarget (2 * h)}

noncomputable def NavierStokes.PositiveRepresentatives.stableQ (h : ℝ) (p : Slow) : ℝ

Stable Q, given by (stableInverse (2 * h) (p.2.2, p.2.1)).1.

Equations

• NavierStokes.PositiveRepresentatives.stableQ h p = (NavierStokes.PositiveRepresentatives.stableInverse (2 * h) (p.2.2, p.2.1)).1

noncomputable def NavierStokes.PositiveRepresentatives.stableEta (h : ℝ) (p : Slow) : ℝ

Stable eta, given by p.2.1 / stableQ h p ^ CoordinateAlgebra.D h.

Equations

• NavierStokes.PositiveRepresentatives.stableEta h p = p.2.1 / NavierStokes.PositiveRepresentatives.stableQ h p ^ NavierStokes.CoordinateAlgebra.D h

noncomputable def NavierStokes.PositiveRepresentatives.stableX (h : ℝ) (p : Slow) : ℝ

Stable X, given by p.1 ^ 2 / (2 * stableQ h p).

Equations

• NavierStokes.PositiveRepresentatives.stableX h p = p.1 ^ 2 / (2 * NavierStokes.PositiveRepresentatives.stableQ h p)

noncomputable def NavierStokes.PositiveRepresentatives.stableInner (h : ℝ) (p : Slow) : ℝ × ℝ

Stable inner, given by (stableX h p, stableEta h p).

Equations

• NavierStokes.PositiveRepresentatives.stableInner h p = (NavierStokes.PositiveRepresentatives.stableX h p, NavierStokes.PositiveRepresentatives.stableEta h p)

theorem NavierStokes.PositiveRepresentatives.stableDomain_open (h : ℝ) : IsOpen (stableDomain h)

theorem NavierStokes.PositiveRepresentatives.stableQ_spec {h : ℝ} {p : Slow} (hp : p ∈ stableDomain h) : 0 < stableQ h p ∧ SimilarityCoordinates.forwardScalar (2 * h) p.2.1 (stableQ h p) = p.2.2

theorem NavierStokes.PositiveRepresentatives.stableQ_smoothAt {h : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) {p : Slow} (hp : p ∈ stableDomain h) : ContDiffAt ℝ (↑⊤) (stableQ h) p

theorem NavierStokes.PositiveRepresentatives.stableInner_smoothAt {h : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) {p : Slow} (hp : p ∈ stableDomain h) : ContDiffAt ℝ (↑⊤) (stableInner h) p

theorem NavierStokes.PositiveRepresentatives.positiveTime_mem_stableDomain {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Slow} (hR : 0 < p.1) (hT : 0 < p.2.2) : p ∈ stableDomain h

theorem NavierStokes.PositiveRepresentatives.stableQ_eq_chartQ {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Slow} (hp : 0 < p.2.2) : stableQ h p = SimilarityHomogeneity.chartQ h p

theorem NavierStokes.PositiveRepresentatives.stableInner_eq_chartInner {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Slow} (hp : 0 < p.2.2) : stableInner h p = SimilarityHomogeneity.chartInner h p

theorem NavierStokes.PositiveRepresentatives.referenceCompact_subset_stableDomain {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : PrimaryRepresentatives.referenceCompact h a b ⊆ stableDomain h

theorem NavierStokes.PositiveRepresentatives.stableQ_bounds_reference {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) {p : Slow} (hp : p ∈ PrimaryRepresentatives.referenceCompact h a b) : stableQ h p ∈ Set.Icc (1 / 2) 2 ∧ stableX h p ∈ Set.Icc a b

theorem NavierStokes.PositiveRepresentatives.stableEta_sq {h : ℝ} {p : Slow} (hp : p ∈ stableDomain h) : stableEta h p ^ 2 = p.2.1 ^ 2 * stableQ h p ^ (2 * h) / stableQ h p

theorem NavierStokes.PositiveRepresentatives.stableEta_mem_reference {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) {p : Slow} (hp : p ∈ PrimaryRepresentatives.referenceCompact h a b) : stableEta h p ∈ Set.Icc (-1) 1

theorem NavierStokes.PositiveRepresentatives.reference_zeroTime_axial_ne {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) {p : Slow} (hp : p ∈ PrimaryRepresentatives.referenceCompact h a b) (ht : p.2.2 = 0) : p.2.1 ≠ 0

noncomputable def NavierStokes.PositiveRepresentatives.boundedDomain (h a b : ℝ) : Set Slow

An open stable-branch neighborhood with fixed radial and similarity coordinate bounds. Its positive-time part is the physical domain.

Equations

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

theorem NavierStokes.PositiveRepresentatives.boundedDomain_open {h : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (a b : ℝ) : IsOpen (boundedDomain h a b)

theorem NavierStokes.PositiveRepresentatives.referenceCompact_subset_boundedDomain {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : PrimaryRepresentatives.referenceCompact h a b ⊆ boundedDomain h a b

noncomputable def NavierStokes.PositiveRepresentatives.openGrid (n : ℕ) (k : SlotColoring.Grid) : Set Slow

Three-mesh open box; the actual enlarged support uses two meshes.

Equations

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

noncomputable def NavierStokes.PositiveRepresentatives.positiveCell (n : ℕ) (k : SlotColoring.Grid) : Set Slow

Positive cell, given by openGrid n k ∩ positiveTime.

Equations

• NavierStokes.PositiveRepresentatives.positiveCell n k = NavierStokes.PositiveRepresentatives.openGrid n k ∩ NavierStokes.PositiveRepresentatives.positiveTime

theorem NavierStokes.PositiveRepresentatives.positiveCell_open (n : ℕ) (k : SlotColoring.Grid) : IsOpen (positiveCell n k)

theorem NavierStokes.PositiveRepresentatives.positiveCell_convex (n : ℕ) (k : SlotColoring.Grid) : Convex ℝ (positiveCell n k)

theorem NavierStokes.PositiveRepresentatives.openGrid_subset_gridBox (n : ℕ) (k : SlotColoring.Grid) : openGrid n k ⊆ PrimaryRepresentatives.gridBox n k 3

theorem NavierStokes.PositiveRepresentatives.gridBox_two_subset_openGrid {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : PrimaryRepresentatives.gridBox n k 2 ⊆ openGrid n k

theorem NavierStokes.PositiveRepresentatives.representative_mem_cell (K : Set Slow) (L : ActiveLabel K) : representative K L ∈ positiveCell (↑L).1 (↑L).2

theorem NavierStokes.PositiveRepresentatives.enlarged_positive_subset_cell {n : ℕ} (hn : 1 ≤ n) (k : SlotColoring.Grid) : PrimaryRepresentatives.gridBox n k 2 ∩ positiveTime ⊆ positiveCell n k

theorem NavierStokes.PositiveRepresentatives.mesh_four_tendsto_zero : Filter.Tendsto (fun (n : ℕ) => 4 * SquaredPartition.nativeSpacing n) Filter.atTop (nhds 0)

theorem NavierStokes.PositiveRepresentatives.positiveCell_eventually_subset {K U : Set Slow} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (N : ℕ), ∀ (L : ActiveLabel K), N ≤ (↑L).1 → positiveCell (↑L).1 (↑L).2 ⊆ U

The positive cells eventually lie in any open neighborhood of the compact reference set. No lower bound for their positive time is used.

noncomputable def NavierStokes.PositiveRepresentatives.cellBound (b : ℝ) : ℝ

Cell bound, given by max (2 * Real.sqrt b + 1) 3.

Equations

• NavierStokes.PositiveRepresentatives.cellBound b = max (2 * √b + 1) 3

theorem NavierStokes.PositiveRepresentatives.cellBound_pos (b : ℝ) : 0 < cellBound b

theorem NavierStokes.PositiveRepresentatives.baseChart_norm_bound {a b : ℝ} (ha : 0 < a) {p : Slow} (hp : p ∈ PrimaryRepresentatives.baseChart a b) : √a / 2 ≤ p.1 ∧ ‖p‖ ≤ cellBound b

theorem NavierStokes.PositiveRepresentatives.exists_positive_reference_charts {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : ∃ (N : ℕ), ∀ (L : ActiveLabel (PrimaryRepresentatives.referenceCompact h a b)), N ≤ (↑L).1 → IsOpen (positiveCell (↑L).1 (↑L).2) ∧ Convex ℝ (positiveCell (↑L).1 (↑L).2) ∧ representative (PrimaryRepresentatives.referenceCompact h a b) L ∈ positiveCell (↑L).1 (↑L).2 ∧ PrimaryRepresentatives.gridBox (↑L).1 (↑L).2 2 ∩ positiveTime ⊆ positiveCell (↑L).1 (↑L).2 ∧ ∀ p ∈ positiveCell (↑L).1 (↑L).2, 0 < p.1 ∧ √a / 2 ≤ p.1 ∧ ‖p‖ ≤ cellBound b ∧ 0 < p.2.2 ∧ SimilarityHomogeneity.chartQ h p ∈ Set.Ioo (1 / 4) 4 ∧ SimilarityHomogeneity.chartX h p ∈ Set.Ioo (a / 2) (2 * b)

The same positive representative and a convex open domain work for every positive-time point in its enlarged two-mesh box. All coordinate range constants are uniform as time approaches zero.

Compact bounds use the genuine extension, with physical jet equality

theorem NavierStokes.PositiveRepresentatives.stableQ_eventuallyEq_chartQ {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Slow} (hp : 0 < p.2.2) : stableQ h =ᶠ[nhds p] SimilarityHomogeneity.chartQ h

theorem NavierStokes.PositiveRepresentatives.stableInner_eventuallyEq_chartInner {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Slow} (hp : 0 < p.2.2) : stableInner h =ᶠ[nhds p] SimilarityHomogeneity.chartInner h

theorem NavierStokes.PositiveRepresentatives.iteratedFDeriv_eq_of_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : Slow → E} {p : Slow} (he : f =ᶠ[nhds p] g) (n : ℕ) : iteratedFDeriv ℝ n f p = iteratedFDeriv ℝ n g p

theorem NavierStokes.PositiveRepresentatives.stableQ_iteratedFDeriv_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Slow} (hp : 0 < p.2.2) (n : ℕ) : iteratedFDeriv ℝ n (stableQ h) p = iteratedFDeriv ℝ n (SimilarityHomogeneity.chartQ h) p

theorem NavierStokes.PositiveRepresentatives.stableInner_iteratedFDeriv_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Slow} (hp : 0 < p.2.2) (n : ℕ) : iteratedFDeriv ℝ n (stableInner h) p = iteratedFDeriv ℝ n (SimilarityHomogeneity.chartInner h) p

theorem NavierStokes.PositiveRepresentatives.compact_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set Slow} (hK : IsCompact K) {f : Slow → E} (hf : ∀ p ∈ K, ContDiffAt ℝ (↑⊤) f p) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ p ∈ K, ‖iteratedFDeriv ℝ n f p‖ ≤ C

noncomputable def NavierStokes.PositiveRepresentatives.stablePullback (h exponent : ℝ) (f : ℝ × ℝ → ℝ) (p : Slow) : ℝ

Stable pullback, given by stableQ h p ^ exponent * f (stableInner h p).

Equations

• NavierStokes.PositiveRepresentatives.stablePullback h exponent f p = NavierStokes.PositiveRepresentatives.stableQ h p ^ exponent * f (NavierStokes.PositiveRepresentatives.stableInner h p)

noncomputable def NavierStokes.PositiveRepresentatives.physicalPullback (h exponent : ℝ) (f : ℝ × ℝ → ℝ) (p : Slow) : ℝ

Physical pullback, given by SimilarityHomogeneity.chartQ h p ^ exponent * f (SimilarityHomogeneity.chartInner h p).

Equations

• NavierStokes.PositiveRepresentatives.physicalPullback h exponent f p = NavierStokes.SimilarityHomogeneity.chartQ h p ^ exponent * f (NavierStokes.SimilarityHomogeneity.chartInner h p)

theorem NavierStokes.PositiveRepresentatives.stablePullback_smoothAt {h : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (exponent : ℝ) {f : ℝ × ℝ → ℝ} {p : Slow} (hp : p ∈ stableDomain h) (hf : ContDiffAt ℝ (↑⊤) f (stableInner h p)) : ContDiffAt ℝ (↑⊤) (stablePullback h exponent f) p

theorem NavierStokes.PositiveRepresentatives.stablePullback_eventuallyEq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (exponent : ℝ) (f : ℝ × ℝ → ℝ) {p : Slow} (hp : 0 < p.2.2) : stablePullback h exponent f =ᶠ[nhds p] physicalPullback h exponent f

theorem NavierStokes.PositiveRepresentatives.physicalPullback_uniform_jet_bound {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) (exponent : ℝ) {f : ℝ × ℝ → ℝ} (hf : ∀ x ∈ Set.Icc a b ×ˢ Set.Icc (-1) 1, ContDiffAt ℝ (↑⊤) f x) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ p ∈ PrimaryRepresentatives.referenceCompact h a b, 0 < p.2.2 → ‖iteratedFDeriv ℝ n (physicalPullback h exponent f) p‖ ≤ C

Actual physical derivatives have one compact bound down to arbitrarily small positive time. The boundary values used in the proof are the genuine stable extension, not derivatives of a totalized inverse at zero time.

Compact reference data are transferred only at positive time

theorem NavierStokes.PositiveRepresentatives.shearVector_eq_on_positive {F G Fext Gext : Slow → ℝ} (hF : Set.EqOn F Fext positiveTime) (hG : Set.EqOn G Gext positiveTime) : Set.EqOn (PhaseEstimates.shearVector F G) (PhaseEstimates.shearVector Fext Gext) positiveTime

noncomputable def NavierStokes.PositiveRepresentatives.ActiveLabel.toClosed {K : Set Slow} (L : ActiveLabel K) : PrimaryRepresentatives.ActiveLabel K

To closed, given by ⟨L.val, L.property.1, representative K L, representative_mem K L, representative_mem_tsupport K L⟩.

Equations

• L.toClosed = ⟨↑L, ⋯⟩

@[simp]

theorem NavierStokes.PositiveRepresentatives.ActiveLabel.toClosed_val {K : Set Slow} (L : ActiveLabel K) : ↑L.toClosed = ↑L

theorem NavierStokes.PositiveRepresentatives.representative_parameter_bounds {K : Set Slow} (hK : IsCompact K) {F Fext : Slow → ℝ} {g gext : Slow → MovingFrameODE.Plane} (hF : ContinuousOn Fext K) (hg : ContinuousOn gext K) (hR : ∀ p ∈ K, 0 < p.1) (hc : ∀ p ∈ K, PrimaryRepresentatives.ReferenceCone (Fext p) (gext p)) (hFeq : Set.EqOn F Fext (positivePart K)) (hgeq : Set.EqOn g gext (positivePart K)) : ∃ (M : ℝ), 1 ≤ M ∧ ∀ (L : ActiveLabel K), PrimaryRepresentatives.ParameterBounds M (representative K L).1 (F (representative K L)) (g (representative K L))

The reference functions on the compact closure are explicit extensions. Only their values at the positive representatives are identified with the physical data. No equality at zero time is assumed.

theorem NavierStokes.PositiveRepresentatives.representative_target_margin {K : Set Slow} (hK : IsCompact K) {F Fext : Slow → ℝ} {g gext T Text : Slow → MovingFrameODE.Plane} (hF : ContinuousOn Fext K) (hg : ContinuousOn gext K) (hT : ContinuousOn Text K) (hc : ∀ p ∈ K, PrimaryRepresentatives.ReferenceCone (Fext p) (gext p)) (ht : ∀ p ∈ K, PrimaryRepresentatives.TargetCone (Fext p) (gext p) (Text p)) (hFeq : Set.EqOn F Fext (positivePart K)) (hgeq : Set.EqOn g gext (positivePart K)) (hTeq : Set.EqOn T Text (positivePart K)) : ∃ (u : ℝ) (eta : ℝ), 0 < u ∧ 0 < eta ∧ ∃ (N : ℕ), ∀ (L : ActiveLabel K), N ≤ (↑L).1 → ∀ p ∈ positivePart K, p ∈ PrimaryRepresentatives.gridBox (↑L).1 (↑L).2 2 → inner ℝ (T p) (PrimaryRepresentatives.normalDirection (g (representative K L))) ≤ -eta ∧ |PrimaryRepresentatives.c0 (F (representative K L)) (g (representative K L)) * inner ℝ (T p) (PrimaryRepresentatives.transverseDirection (g (representative K L))) / inner ℝ (T p) (PrimaryRepresentatives.normalDirection (g (representative K L)))| + eta ≤ PrimaryRepresentatives.slopeRatio u

The target-direction margin is transferred from continuous extended reference data to the actual positive-time target and representative.