Actual grid representatives and uniform primary reference parameters

Representatives are selected in the intersection of the actual closed mask support and the fixed closed active set. The enlarged-box distance is then a consequence of the mesh, rather than a hypothesis on the selected point.

@[reducible, inline]

abbrev NavierStokes.PrimaryRepresentatives.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.PrimaryRepresentatives.Slow = NavierStokes.PhaseCalculus.Slow

@[reducible, inline]

abbrev NavierStokes.PrimaryRepresentatives.Plane : Type

Plane: an abbreviation for MovingFrameODE.Plane.

Equations

• NavierStokes.PrimaryRepresentatives.Plane = NavierStokes.MovingFrameODE.Plane

@[reducible, inline]

abbrev NavierStokes.PrimaryRepresentatives.Grid : Type

Grid: an abbreviation for SlotColoring.Grid.

Equations

• NavierStokes.PrimaryRepresentatives.Grid = NavierStokes.SlotColoring.Grid

@[reducible, inline]

abbrev NavierStokes.PrimaryRepresentatives.Label : Type

Label: an abbreviation for PartitionedCovariance.UnsignedLabel.

Equations

• NavierStokes.PrimaryRepresentatives.Label = NavierStokes.PartitionedCovariance.UnsignedLabel

@[reducible, inline]

abbrev NavierStokes.PrimaryRepresentatives.Position : Type

Position: an abbreviation for SlotColoring.Position.

Equations

• NavierStokes.PrimaryRepresentatives.Position = NavierStokes.SlotColoring.Position

noncomputable def NavierStokes.PrimaryRepresentatives.position (q : Slow) : Position

Position, given by ![q.1, q.2.1, q.2.2].

Equations

• NavierStokes.PrimaryRepresentatives.position q = ![q.1, q.2.1, q.2.2]

noncomputable def NavierStokes.PrimaryRepresentatives.slow (x : Position) : Slow

Slow, given by (x 0, (x 1, x 2)).

Equations

• NavierStokes.PrimaryRepresentatives.slow x = (x 0, x 1, x 2)

@[simp]

theorem NavierStokes.PrimaryRepresentatives.position_slow (x : Position) : position (slow x) = x

@[simp]

theorem NavierStokes.PrimaryRepresentatives.slow_position (q : Slow) : slow (position q) = q

theorem NavierStokes.PrimaryRepresentatives.position_smooth : ContDiff ℝ (↑⊤) position

theorem NavierStokes.PrimaryRepresentatives.slow_smooth : ContDiff ℝ (↑⊤) slow

theorem NavierStokes.PrimaryRepresentatives.norm_slow_sub_le {x y : Position} {c : ℝ} (h : ∀ (j : Fin 3), |x j - y j| ≤ c) : ‖slow x - slow y‖ ≤ c

noncomputable def NavierStokes.PrimaryRepresentatives.nativeMask (n : ℕ) (k : Grid) (q : Slow) : ℝ

Native mask, given by SquaredPartition.slowMask n k (position q).

Equations

• NavierStokes.PrimaryRepresentatives.nativeMask n k q = NavierStokes.SquaredPartition.slowMask n k (NavierStokes.PrimaryRepresentatives.position q)

noncomputable def NavierStokes.PrimaryRepresentatives.gridBox (n : ℕ) (k : Grid) (a : ℝ) : Set Slow

Grid box, given by {q | ∀ j, |position q j - SquaredPartition.nativeSpacing n * (k j : ℝ)| ≤ a * SquaredPartition.nativeSpacing n}.

Equations

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

theorem NavierStokes.PrimaryRepresentatives.gridBox_closed (n : ℕ) (k : Grid) (a : ℝ) : IsClosed (gridBox n k a)

theorem NavierStokes.PrimaryRepresentatives.nativeMask_smooth (n : ℕ) (k : Grid) : ContDiff ℝ (↑⊤) (nativeMask n k)

theorem NavierStokes.PrimaryRepresentatives.nativeMask_tsupport_subset {n : ℕ} (hn : 1 ≤ n) (k : Grid) : tsupport (nativeMask n k) ⊆ gridBox n k 1

theorem NavierStokes.PrimaryRepresentatives.gridBox_distance {n : ℕ} {k : Grid} {a b : ℝ} {q q₀ : Slow} (hq : q ∈ gridBox n k a) (h₀ : q₀ ∈ gridBox n k b) : ‖q - q₀‖ ≤ (a + b) * SquaredPartition.nativeSpacing n

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

Exactly the labels whose closed mask support meets the closed active set.

Equations

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

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

Representative, given by Classical.choose L.property.2.

Equations

• NavierStokes.PrimaryRepresentatives.representative K L = Classical.choose ⋯

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

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

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

The sharp bound furnished by a one-mesh support and a two-mesh pad.

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

noncomputable def NavierStokes.PrimaryRepresentatives.normalizedSlow (D : ℝ) (n : ℕ) (x : Position) : Slow

Normalized slow, given by slow (SquaredPartition.slowCoordinates D n x).

Equations

• NavierStokes.PrimaryRepresentatives.normalizedSlow D n x = NavierStokes.PrimaryRepresentatives.slow (NavierStokes.SquaredPartition.slowCoordinates D n x)

theorem NavierStokes.PrimaryRepresentatives.width_eq_scaled_spacing (D : ℝ) (n : ℕ) (j : Fin 3) : SlotColoring.width D j n = ChartScales.Q n ^ SlotColoring.axisExponent D j * SquaredPartition.nativeSpacing n

theorem NavierStokes.PrimaryRepresentatives.physicalBox_normalizes (D : ℝ) (L : SlotColoring.Label) {x : Position} (hx : x ∈ SlotColoring.physicalBox D L) : normalizedSlow D L.1 x ∈ gridBox L.1 L.2.1 2

theorem NavierStokes.PrimaryRepresentatives.physicalMask_nativeMask (D : ℝ) (L : Label) (q : ℝ) (x : Position) : PartitionedCovariance.mask D L q x = SquaredPartition.dyadicMask (↑L.1) q * nativeMask L.1 L.2 (normalizedSlow D L.1 x)

theorem NavierStokes.PrimaryRepresentatives.physicalMask_active (K : Set Slow) (D : ℝ) (L : Label) (hL : 1 ≤ L.1) {q : ℝ} {x : Position} (hx : normalizedSlow D L.1 x ∈ K) (hm : PartitionedCovariance.mask D L q x ≠ 0) : ∃ (A : ActiveLabel K), ↑A = L

Every nonzero actual physical mask on the active set produces one of the labels for which the representative was constructed.

theorem NavierStokes.PrimaryRepresentatives.grid_mesh_tendsto_zero : Filter.Tendsto (fun (n : ℕ) => 3 / ChartScales.S n ^ 3) Filter.atTop (nhds 0)

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

All enlarged boxes of active sufficiently fine labels lie in a single prescribed open base-control chart.

Reference frame and exact unstable-mode parameters

noncomputable def NavierStokes.PrimaryRepresentatives.normalDirection (g : Plane) : Plane

Normal direction, given by ‖g‖⁻¹ • g.

Equations

• NavierStokes.PrimaryRepresentatives.normalDirection g = ‖g‖⁻¹ • g

noncomputable def NavierStokes.PrimaryRepresentatives.transverseDirection (g : Plane) : Plane

Transverse direction, given by -MovingFrameODE.quarterTurn (normalDirection g).

Equations

• NavierStokes.PrimaryRepresentatives.transverseDirection g = -NavierStokes.MovingFrameODE.quarterTurn (NavierStokes.PrimaryRepresentatives.normalDirection g)

noncomputable def NavierStokes.PrimaryRepresentatives.coupling (F : ℝ) (g : Plane) : ℝ

Coupling, given by 2 * F * normalDirection g 0.

Equations

• NavierStokes.PrimaryRepresentatives.coupling F g = 2 * F * (NavierStokes.PrimaryRepresentatives.normalDirection g).ofLp 0

noncomputable def NavierStokes.PrimaryRepresentatives.lambda0 (F : ℝ) (g : Plane) : ℝ

Lambda0, given by Real.sqrt (-(coupling F g) * (coupling F g + ‖g‖)).

Equations

• NavierStokes.PrimaryRepresentatives.lambda0 F g = √(-NavierStokes.PrimaryRepresentatives.coupling F g * (NavierStokes.PrimaryRepresentatives.coupling F g + ‖g‖))

noncomputable def NavierStokes.PrimaryRepresentatives.c0 (F : ℝ) (g : Plane) : ℝ

C0, given by lambda0 F g / coupling F g.

Equations

• NavierStokes.PrimaryRepresentatives.c0 F g = NavierStokes.PrimaryRepresentatives.lambda0 F g / NavierStokes.PrimaryRepresentatives.coupling F g

structure NavierStokes.PrimaryRepresentatives.ReferenceCone (F : ℝ) (g : Plane) : Prop

Primitive strict shear conditions. The last inequality is the positive opening of the unstable two-dimensional reference system.

• frequency_pos : 0 < F
• theta_neg : g.ofLp 0 < 0
• opening_pos : 0 < 2 * F * g.ofLp 0 + ‖g‖ ^ 2

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.shear_ne_zero {F : ℝ} {g : Plane} (h : ReferenceCone F g) : g ≠ 0

theorem NavierStokes.PrimaryRepresentatives.referenceCone_of_shear_coordinates {F a b : ℝ} (hF : 0 < F) (ha : 0 < a) (hv : 2 * a < a ^ 2 + b ^ 2) : ReferenceCone F (F • !₂[-a, b])

The manuscript's shear coordinates give the primitive reference cone from a > 0 and a²+b² > 2a.

theorem NavierStokes.PrimaryRepresentatives.normalDirection_unit {g : Plane} (hg : g ≠ 0) : ‖normalDirection g‖ = 1

theorem NavierStokes.PrimaryRepresentatives.transverseDirection_unit {g : Plane} (hg : g ≠ 0) : ‖transverseDirection g‖ = 1

theorem NavierStokes.PrimaryRepresentatives.quarterTurn_transverseDirection (g : Plane) : MovingFrameODE.quarterTurn (transverseDirection g) = normalDirection g

theorem NavierStokes.PrimaryRepresentatives.norm_smul_normalDirection {g : Plane} (hg : g ≠ 0) : ‖g‖ • normalDirection g = g

theorem NavierStokes.PrimaryRepresentatives.transverseDirection_inner_shear (g : Plane) : inner ℝ (transverseDirection g) g = 0

theorem NavierStokes.PrimaryRepresentatives.normalDirection_theta (g : Plane) : (normalDirection g).ofLp 0 = g.ofLp 0 / ‖g‖

theorem NavierStokes.PrimaryRepresentatives.coupling_eq (F : ℝ) (g : Plane) : coupling F g = 2 * F * g.ofLp 0 / ‖g‖

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.coupling_neg {F : ℝ} {g : Plane} (h : ReferenceCone F g) : coupling F g < 0

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.normalDirection_theta_neg {F : ℝ} {g : Plane} (h : ReferenceCone F g) : (normalDirection g).ofLp 0 < 0

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.coupling_add_norm_pos {F : ℝ} {g : Plane} (h : ReferenceCone F g) : 0 < coupling F g + ‖g‖

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.lambda0_pos {F : ℝ} {g : Plane} (h : ReferenceCone F g) : 0 < lambda0 F g

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.lambda0_sq {F : ℝ} {g : Plane} (h : ReferenceCone F g) : lambda0 F g ^ 2 = -coupling F g * (coupling F g + ‖g‖)

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.c0_neg {F : ℝ} {g : Plane} (h : ReferenceCone F g) : c0 F g < 0

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.lambda0_div_c0 {F : ℝ} {g : Plane} (h : ReferenceCone F g) : lambda0 F g / c0 F g = 2 * F * (normalDirection g).ofLp 0

theorem NavierStokes.PrimaryRepresentatives.ReferenceCone.lambda0_mul_c0 {F : ℝ} {g : Plane} (h : ReferenceCone F g) : lambda0 F g * c0 F g = -(2 * F * (normalDirection g).ofLp 0 + ‖g‖)

theorem NavierStokes.PrimaryRepresentatives.normalDirection_continuousOn {X : Type u_1} [TopologicalSpace X] {K : Set X} {g : X → Plane} (hg : ContinuousOn g K) (hne : ∀ q ∈ K, g q ≠ 0) : ContinuousOn (fun (q : X) => normalDirection (g q)) K

theorem NavierStokes.PrimaryRepresentatives.transverseDirection_continuousOn {X : Type u_1} [TopologicalSpace X] {K : Set X} {g : X → Plane} (hg : ContinuousOn g K) (hne : ∀ q ∈ K, g q ≠ 0) : ContinuousOn (fun (q : X) => transverseDirection (g q)) K

theorem NavierStokes.PrimaryRepresentatives.coupling_continuousOn {X : Type u_1} [TopologicalSpace X] {K : Set X} {F : X → ℝ} {g : X → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hne : ∀ q ∈ K, g q ≠ 0) : ContinuousOn (fun (q : X) => coupling (F q) (g q)) K

theorem NavierStokes.PrimaryRepresentatives.lambda0_continuousOn {X : Type u_1} [TopologicalSpace X] {K : Set X} {F : X → ℝ} {g : X → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hne : ∀ q ∈ K, g q ≠ 0) : ContinuousOn (fun (q : X) => lambda0 (F q) (g q)) K

theorem NavierStokes.PrimaryRepresentatives.c0_continuousOn {X : Type u_1} [TopologicalSpace X] {K : Set X} {F : X → ℝ} {g : X → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) : ContinuousOn (fun (q : X) => c0 (F q) (g q)) K

noncomputable def NavierStokes.PrimaryRepresentatives.parameterScalars (F : Slow → ℝ) (g : Slow → Plane) (q : Slow) : Fin 9 → ℝ

Parameter scalars, given by ![q.1, F q, ‖g q‖, lambda0 (F q) (g q), c0 (F q) (g q), q.1⁻¹, ‖g q‖⁻¹, (lambda0 (F q) (g q))⁻¹, (c0 (F q) (g q))⁻¹].

Equations

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

theorem NavierStokes.PrimaryRepresentatives.parameterScalars_continuousOn {K : Set Slow} {F : Slow → ℝ} {g : Slow → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hR : ∀ q ∈ K, 0 < q.1) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) : ContinuousOn (parameterScalars F g) K

structure NavierStokes.PrimaryRepresentatives.ParameterBounds (M R F : ℝ) (g : Plane) : Prop

The same constant controls every representative parameter and reciprocal.

• radius : R ≤ M
• frequency : |F| ≤ M
• shear : ‖g‖ ≤ M
• lambda : lambda0 F g ≤ M
• ratio : |c0 F g| ≤ M
• radius_inv : R⁻¹ ≤ M
• shear_inv : ‖g‖⁻¹ ≤ M
• lambda_inv : (lambda0 F g)⁻¹ ≤ M
• ratio_inv : |c0 F g|⁻¹ ≤ M

theorem NavierStokes.PrimaryRepresentatives.compact_parameter_bounds {K : Set Slow} (hK : IsCompact K) {F : Slow → ℝ} {g : Slow → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hR : ∀ q ∈ K, 0 < q.1) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) : ∃ (M : ℝ), 1 ≤ M ∧ ∀ q ∈ K, ParameterBounds M q.1 (F q) (g q)

theorem NavierStokes.PrimaryRepresentatives.ParameterBounds.mono {M M' R F : ℝ} {g : Plane} (h : ParameterBounds M R F g) (hMM' : M ≤ M') : ParameterBounds M' R F g

theorem NavierStokes.PrimaryRepresentatives.ParameterBounds.positive_lower {M R F : ℝ} {g : Plane} (h : ParameterBounds M R F g) (hM : 1 ≤ M) (hR : 0 < R) (hc : ReferenceCone F g) : M⁻¹ ≤ R ∧ M⁻¹ ≤ ‖g‖ ∧ M⁻¹ ≤ lambda0 F g ∧ M⁻¹ ≤ |c0 F g|

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

A fixed compact set from the actual normalized similarity range

noncomputable def NavierStokes.PrimaryRepresentatives.activeReference (h a b : ℝ) : Set Slow

Normalized active points, including the limiting time face T = 0.

Equations

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

noncomputable def NavierStokes.PrimaryRepresentatives.referenceBox (a b : ℝ) : Set Slow

Reference box, given by Icc (Real.sqrt a) (2 * Real.sqrt b) ×ˢ (Icc (-2 : ℝ) 2 ×ˢ Icc (0 : ℝ) 2).

Equations

• NavierStokes.PrimaryRepresentatives.referenceBox a b = Set.Icc (√a) (2 * √b) ×ˢ Set.Icc (-2) 2 ×ˢ Set.Icc 0 2

noncomputable def NavierStokes.PrimaryRepresentatives.referenceCompact (h a b : ℝ) : Set Slow

Reference compact, given by closure (activeReference h a b).

Equations

• NavierStokes.PrimaryRepresentatives.referenceCompact h a b = closure (NavierStokes.PrimaryRepresentatives.activeReference h a b)

theorem NavierStokes.PrimaryRepresentatives.activeReference_subset_box {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : activeReference h a b ⊆ referenceBox a b

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

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

theorem NavierStokes.PrimaryRepresentatives.referenceCompact_radius_pos {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) {q : Slow} (hq : q ∈ referenceCompact h a b) : 0 < q.1

noncomputable def NavierStokes.PrimaryRepresentatives.baseChart (a b : ℝ) : Set Slow

One explicit convex chart containing the whole normalized compact set.

Equations

• NavierStokes.PrimaryRepresentatives.baseChart a b = Set.Ioo (√a / 2) (2 * √b + 1) ×ˢ Set.Ioo (-3) 3 ×ˢ Set.Ioo (-1) 3

theorem NavierStokes.PrimaryRepresentatives.baseChart_open (a b : ℝ) : IsOpen (baseChart a b)

theorem NavierStokes.PrimaryRepresentatives.baseChart_convex (a b : ℝ) : Convex ℝ (baseChart a b)

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

theorem NavierStokes.PrimaryRepresentatives.reference_enlarged_eventually_in_chart {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a ≤ b) : ∃ (N : ℕ), ∀ (L : ActiveLabel (referenceCompact h a b)), N ≤ (↑L).1 → gridBox (↑L).1 (↑L).2 2 ⊆ baseChart a b

theorem NavierStokes.PrimaryRepresentatives.normalizedSlow_coordinates (D : ℝ) (n : ℕ) (x : Position) : normalizedSlow D n x = (x 0 / ChartScales.Q n ^ (1 / 2), x 1 / ChartScales.Q n ^ D, x 2 / ChartScales.Q n)

theorem NavierStokes.PrimaryRepresentatives.physicalMask_normalized_mem {h a b : ℝ} (L : Label) {q : ℝ} {x : 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) : normalizedSlow (CoordinateAlgebra.D h) L.1 x ∈ referenceCompact h a b

The physical similarity equation and the actual dyadic mask put every active point into the same compact reference set, independent of its label.

theorem NavierStokes.PrimaryRepresentatives.physicalMask_has_representative {h a b : ℝ} (L : Label) (hL : 1 ≤ L.1) {q : ℝ} {x : 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 (referenceCompact h a b)), ↑A = L

One target-direction parameter, with uniform mixed-point slack

noncomputable def NavierStokes.PrimaryRepresentatives.targetRatio (F : ℝ) (g T : Plane) : ℝ

Target ratio, given by |c0 F g * ⟪T, transverseDirection g⟫_ℝ / ⟪T, normalDirection g⟫_ℝ|.

Equations

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

structure NavierStokes.PrimaryRepresentatives.TargetCone (F : ℝ) (g T : Plane) : Prop

T is a continuous target direction, including at zero-amplitude edges.

• inward : inner ℝ T (normalDirection g) < 0
• ratio_lt_one : targetRatio F g T < 1

noncomputable def NavierStokes.PrimaryRepresentatives.slopeRatio (u : ℝ) : ℝ

Slope ratio, given by u / Real.sqrt (1 + u ^ 2).

Equations

• NavierStokes.PrimaryRepresentatives.slopeRatio u = u / √(1 + u ^ 2)

theorem NavierStokes.PrimaryRepresentatives.exists_slopeRatio_gt {r : ℝ} (hr : 0 ≤ r) (hr1 : r < 1) : ∃ (u : ℝ), 0 < u ∧ r < slopeRatio u

theorem NavierStokes.PrimaryRepresentatives.slopeRatio_lt_one (u : ℝ) : slopeRatio u < 1

theorem NavierStokes.PrimaryRepresentatives.targetRatio_continuousOn {K : Set Slow} {F : Slow → ℝ} {g T : Slow → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hT : ContinuousOn T K) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) (ht : ∀ q ∈ K, TargetCone (F q) (g q) (T q)) : ContinuousOn (fun (q : Slow) => targetRatio (F q) (g q) (T q)) K

theorem NavierStokes.PrimaryRepresentatives.compact_target_choice {K : Set Slow} (hK : IsCompact K) {F : Slow → ℝ} {g T : Slow → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hT : ContinuousOn T K) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) (ht : ∀ q ∈ K, TargetCone (F q) (g q) (T q)) : ∃ (u : ℝ) (η : ℝ), 0 < u ∧ 0 < η ∧ ∀ q ∈ K, inner ℝ (T q) (normalDirection (g q)) ≤ -η ∧ targetRatio (F q) (g q) (T q) + η ≤ slopeRatio u

theorem NavierStokes.PrimaryRepresentatives.compact_diagonal_positive {K : Set Slow} (hK : IsCompact K) {f : Slow × Slow → ℝ} (hf : ContinuousOn f (K ×ˢ K)) (hpos : ∀ q ∈ K, 0 < f (q, q)) : ∃ (δ : ℝ), 0 < δ ∧ ∀ q₀ ∈ K, ∀ q ∈ K, dist q q₀ < δ → 0 < f (q₀, q)

A continuous positive diagonal on a compact set stays positive at nearby pairs, with one distance independent of the base point.

theorem NavierStokes.PrimaryRepresentatives.compact_mixed_target {K : Set Slow} (hK : IsCompact K) {F : Slow → ℝ} {g T : Slow → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hT : ContinuousOn T K) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) (ht : ∀ q ∈ K, TargetCone (F q) (g q) (T q)) : ∃ (u : ℝ) (δ : ℝ), 0 < u ∧ 0 < δ ∧ ∀ q₀ ∈ K, ∀ q ∈ K, dist q q₀ < δ → inner ℝ (T q) (normalDirection (g q₀)) < 0 ∧ |c0 (F q₀) (g q₀) * inner ℝ (T q) (transverseDirection (g q₀)) / inner ℝ (T q) (normalDirection (g q₀))| < slopeRatio u

theorem NavierStokes.PrimaryRepresentatives.representative_target_choice {K : Set Slow} (hK : IsCompact K) {F : Slow → ℝ} {g T : Slow → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hT : ContinuousOn T K) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) (ht : ∀ q ∈ K, TargetCone (F q) (g q) (T q)) : ∃ (u : ℝ), 0 < u ∧ ∃ (N : ℕ), ∀ (L : ActiveLabel K), N ≤ (↑L).1 → ∀ q ∈ K, q ∈ gridBox (↑L).1 (↑L).2 2 → inner ℝ (T q) (normalDirection (g (representative K L))) < 0 ∧ |c0 (F (representative K L)) (g (representative K L)) * inner ℝ (T q) (transverseDirection (g (representative K L))) / inner ℝ (T q) (normalDirection (g (representative K L)))| < slopeRatio u

A single u works for the actual selected representatives and every active target point in the enlarged boxes of all sufficiently fine labels.

theorem NavierStokes.PrimaryRepresentatives.compact_mixed_target_margin {K : Set Slow} (hK : IsCompact K) {F : Slow → ℝ} {g T : Slow → Plane} (hF : ContinuousOn F K) (hg : ContinuousOn g K) (hT : ContinuousOn T K) (hc : ∀ q ∈ K, ReferenceCone (F q) (g q)) (ht : ∀ q ∈ K, TargetCone (F q) (g q) (T q)) : ∃ (u : ℝ) (η : ℝ) (δ : ℝ), 0 < u ∧ 0 < η ∧ 0 < δ ∧ ∀ q₀ ∈ K, ∀ q ∈ K, dist q q₀ < δ → inner ℝ (T q) (normalDirection (g q₀)) ≤ -η ∧ |c0 (F q₀) (g q₀) * inner ℝ (T q) (transverseDirection (g q₀)) / inner ℝ (T q) (normalDirection (g q₀))| + η ≤ slopeRatio u

The mixed-point cone has a positive numerical margin independent of both points. The single selected u is strictly above the supremum.

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

theorem NavierStokes.PrimaryRepresentatives.targetRatio_smul (F : ℝ) (g T : Plane) {a : ℝ} (ha : a ≠ 0) : targetRatio F g (a • T) = targetRatio F g T

theorem NavierStokes.PrimaryRepresentatives.TargetCone.pos_smul {F : ℝ} {g T : Plane} (h : TargetCone F g T) {a : ℝ} (ha : 0 < a) : TargetCone F g (a • T)