Actual terminal stress factors at the outer edge

The logarithmic edge coordinate is applied to the actual physical heat carrier and to OutgoingTail.tailShape. A positive global physical chart keeps the parameter coefficients smooth without assuming a normalized stress factor.

@[reducible, inline]

abbrev NavierStokes.TerminalEdgeFactor.EdgeParam : Type

Edge param: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.TerminalEdgeFactor.EdgeParam = (ℝ × ℝ)

noncomputable def NavierStokes.TerminalEdgeFactor.timeOf (p : EdgeParam) : ℝ

Time of, given by 1 - Real.exp p.1.

Equations

• NavierStokes.TerminalEdgeFactor.timeOf p = 1 - Real.exp p.1

noncomputable def NavierStokes.TerminalEdgeFactor.axisPoint (p : EdgeParam) : SimilarityProfile.PhysicalPoint

Axis point, given by (timeOf p, (0, p.2)).

Equations

• NavierStokes.TerminalEdgeFactor.axisPoint p = (NavierStokes.TerminalEdgeFactor.timeOf p, 0, p.2)

noncomputable def NavierStokes.TerminalEdgeFactor.chartQ (d : OutgoingTail.TailData) (p : EdgeParam) : ℝ

Chart Q, given by SimilarityProfile.q d.h (axisPoint p).

Equations

• NavierStokes.TerminalEdgeFactor.chartQ d p = NavierStokes.SimilarityProfile.q d.h (NavierStokes.TerminalEdgeFactor.axisPoint p)

noncomputable def NavierStokes.TerminalEdgeFactor.chartEta (d : OutgoingTail.TailData) (p : EdgeParam) : ℝ

Chart eta, given by SimilarityProfile.eta d.h (axisPoint p).

Equations

• NavierStokes.TerminalEdgeFactor.chartEta d p = NavierStokes.SimilarityProfile.eta d.h (NavierStokes.TerminalEdgeFactor.axisPoint p)

noncomputable def NavierStokes.TerminalEdgeFactor.outerRadius (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : ℝ

Outer radius, given by Real.sqrt (2 * chartQ d p * Real.exp (y0 + 3)).

Equations

• NavierStokes.TerminalEdgeFactor.outerRadius d y0 p = √(2 * NavierStokes.TerminalEdgeFactor.chartQ d p * Real.exp (y0 + 3))

noncomputable def NavierStokes.TerminalEdgeFactor.radius (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Radius, given by outerRadius d y0 y.1 * Real.exp (-y.2 / 2).

Equations

• NavierStokes.TerminalEdgeFactor.radius d y0 y = NavierStokes.TerminalEdgeFactor.outerRadius d y0 y.1 * Real.exp (-y.2 / 2)

noncomputable def NavierStokes.TerminalEdgeFactor.chartPoint (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : SimilarityProfile.PhysicalPoint

Chart point, given by radiusPoint (timeOf y.1) (radius d y0 y) y.1.2.

Equations

• NavierStokes.TerminalEdgeFactor.chartPoint d y0 y = NavierStokes.TerminalStress.radiusPoint (NavierStokes.TerminalEdgeFactor.timeOf y.1) (NavierStokes.TerminalEdgeFactor.radius d y0 y) y.1.2

theorem NavierStokes.TerminalEdgeFactor.timeOf_lt_one (p : EdgeParam) : timeOf p < 1

theorem NavierStokes.TerminalEdgeFactor.timeOf_contDiff : ContDiff ℝ (↑⊤) timeOf

theorem NavierStokes.TerminalEdgeFactor.axisPoint_contDiff : ContDiff ℝ (↑⊤) axisPoint

theorem NavierStokes.TerminalEdgeFactor.chartQ_pos (d : OutgoingTail.TailData) (p : EdgeParam) : 0 < chartQ d p

theorem NavierStokes.TerminalEdgeFactor.chartQ_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (chartQ d)

theorem NavierStokes.TerminalEdgeFactor.chartEta_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (chartEta d)

theorem NavierStokes.TerminalEdgeFactor.outerRadius_pos (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : 0 < outerRadius d y0 p

theorem NavierStokes.TerminalEdgeFactor.outerRadius_contDiff (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (outerRadius d y0)

theorem NavierStokes.TerminalEdgeFactor.radius_pos (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : 0 < radius d y0 y

theorem NavierStokes.TerminalEdgeFactor.radius_contDiff (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (radius d y0)

theorem NavierStokes.TerminalEdgeFactor.chartPoint_contDiff (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (chartPoint d y0)

theorem NavierStokes.TerminalEdgeFactor.radius_square (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : radius d y0 y ^ 2 = 2 * chartQ d y.1 * Real.exp (y0 + 3 - y.2)

theorem NavierStokes.TerminalEdgeFactor.chartX (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : SimilarityProfile.X d.h (chartPoint d y0 y) = Real.exp (y0 + 3 - y.2)

theorem NavierStokes.TerminalEdgeFactor.chart_logX (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : Real.log (SimilarityProfile.X d.h (chartPoint d y0 y)) = y0 + 3 - y.2

noncomputable def NavierStokes.TerminalEdgeFactor.carrier (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Carrier, given by physicalHeat C (1 + d.h) (chartPoint d y0 y).

Equations

• NavierStokes.TerminalEdgeFactor.carrier C d y0 y = NavierStokes.TerminalStress.physicalHeat C (1 + d.h) (NavierStokes.TerminalEdgeFactor.chartPoint d y0 y)

theorem NavierStokes.TerminalEdgeFactor.carrier_eq (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : carrier C d y0 y = TerminalStress.heatAmplitude C (1 + d.h) (timeOf y.1) (radius d y0 y)

theorem NavierStokes.TerminalEdgeFactor.carrier_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (carrier C d y0)

theorem NavierStokes.TerminalEdgeFactor.carrier_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : 0 < carrier C d y0 y

noncomputable def NavierStokes.TerminalEdgeFactor.carrierRadial (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Carrier radial, given by radius d y0 y * SimilarityProfile.partialS (physicalHeat C (1 + d.h)) (chartPoint d y0 y).

Equations

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

theorem NavierStokes.TerminalEdgeFactor.carrierRadial_eq (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : carrierRadial C d y0 y = deriv (TerminalStress.heatAmplitude C (1 + d.h) (timeOf y.1)) (radius d y0 y)

theorem NavierStokes.TerminalEdgeFactor.carrierRadial_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (carrierRadial C d y0)

noncomputable def NavierStokes.TerminalEdgeFactor.denominator (d : OutgoingTail.TailData) (p : EdgeParam) : ℝ

Denominator, given by timeDenominator d.h (timeOf p) p.2.

Equations

• NavierStokes.TerminalEdgeFactor.denominator d p = NavierStokes.TerminalStress.timeDenominator d.h (NavierStokes.TerminalEdgeFactor.timeOf p) p.2

theorem NavierStokes.TerminalEdgeFactor.denominator_pos (d : OutgoingTail.TailData) (p : EdgeParam) : 0 < denominator d p

theorem NavierStokes.TerminalEdgeFactor.denominator_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (denominator d)

noncomputable def NavierStokes.TerminalEdgeFactor.edgeCoordinate (R r : ℝ) : ℝ

A radial logarithmic distance, with its outer radius kept explicit.

Equations

• NavierStokes.TerminalEdgeFactor.edgeCoordinate R r = -2 * Real.log (r / R)

theorem NavierStokes.TerminalEdgeFactor.edgeCoordinate_hasDerivAt {R r : ℝ} (hR : 0 < R) (hr : 0 < r) : HasDerivAt (edgeCoordinate R) (-2 / r) r

theorem NavierStokes.TerminalEdgeFactor.edgeCoordinate_nonpos {R r : ℝ} (hR : 0 < R) (hRr : R ≤ r) : edgeCoordinate R r ≤ 0

theorem NavierStokes.TerminalEdgeFactor.radius_edgeCoordinate (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : radius d y0 (p, edgeCoordinate (outerRadius d y0 p) r) = r

theorem NavierStokes.TerminalEdgeFactor.edgeCoordinate_radius (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : edgeCoordinate (outerRadius d y0 y.1) (radius d y0 y) = y.2

theorem NavierStokes.TerminalEdgeFactor.physical_logX (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : Real.log (SimilarityProfile.X d.h (TerminalStress.radiusPoint (timeOf p) r p.2)) = y0 + 3 - edgeCoordinate (outerRadius d y0 p) r

theorem NavierStokes.TerminalEdgeFactor.integrableOn_Ioi_of_eventually_zero {f : ℝ → ℝ} {r : ℝ} (hr : 0 < r) (hf : ContinuousOn f (Set.Ioi 0)) (hz : f =ᶠ[Filter.atTop] fun (x : ℝ) => 0) : MeasureTheory.IntegrableOn f (Set.Ioi r) MeasureTheory.volume

Continuous positive-radius functions with a zero tail are genuinely integrable.

noncomputable def NavierStokes.TerminalEdgeFactor.radialFlatDensity (c : ℝ) (j : ℕ) (a : ℝ → ℝ) (R u : ℝ) : ℝ

Radial flat density, given by (2 / u) * FlatPrimitive.integrand c j a (edgeCoordinate R u).

Equations

• NavierStokes.TerminalEdgeFactor.radialFlatDensity c j a R u = 2 / u * NavierStokes.FlatPrimitive.integrand c j a (NavierStokes.TerminalEdgeFactor.edgeCoordinate R u)

theorem NavierStokes.TerminalEdgeFactor.radialFlatDensity_integrable {c R r : ℝ} (hc : 0 < c) (hR : 0 < R) (hr : 0 < r) (j : ℕ) {a : ℝ → ℝ} (ha : Continuous a) : MeasureTheory.IntegrableOn (radialFlatDensity c j a R) (Set.Ioi r) MeasureTheory.volume

theorem NavierStokes.TerminalEdgeFactor.radialFlatDensity_integral {c R r : ℝ} (hc : 0 < c) (hR : 0 < R) (hr : 0 < r) (j : ℕ) {a : ℝ → ℝ} (ha : Continuous a) : ∫ (u : ℝ) in Set.Ioi r, radialFlatDensity c j a R u = FlatPrimitive.primitive c j a (edgeCoordinate R r)

An actual radial-to-edge change of variables, proved by the improper FTC.

theorem NavierStokes.TerminalEdgeFactor.chart_tau_identity (d : OutgoingTail.TailData) (p : EdgeParam) : 1 - timeOf p = chartQ d p * (1 - chartEta d p ^ 2)

theorem NavierStokes.TerminalEdgeFactor.physical_heat_argument (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : 2 * (1 - timeOf y.1) / (radius d y0 y ^ 2 / 2) = 2 * (1 - chartEta d y.1 ^ 2) / Real.exp (y0 + 3 - y.2)

The physical heat argument retains the varying factor 1-eta².

noncomputable def NavierStokes.TerminalEdgeFactor.logTaper (d : OutgoingTail.TailData) (y0 y : ℝ) : ℝ

Log taper, given by tailShape d (y - y0).

Equations

• NavierStokes.TerminalEdgeFactor.logTaper d y0 y = NavierStokes.OutgoingTail.tailShape d (y - y0)

noncomputable def NavierStokes.TerminalEdgeFactor.radialTaper (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : ℝ → ℝ

Radial taper, given by radialSlice (flattening d.h (logTaper d y0)) (timeOf p) p.2.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.logTaper_contDiff (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (logTaper d y0)

theorem NavierStokes.TerminalEdgeFactor.logTaper_hasDerivAt (d : OutgoingTail.TailData) (y0 y : ℝ) : HasDerivAt (logTaper d y0) (OutgoingTail.tailShapeDeriv d (y - y0)) y

theorem NavierStokes.TerminalEdgeFactor.logTaper_deriv_at_radius (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : deriv (logTaper d y0) (Real.log (SimilarityProfile.X d.h (TerminalStress.radiusPoint (timeOf p) r p.2))) = FlatCutoff.edge 4 (edgeCoordinate (outerRadius d y0 p) r) / edgeCoordinate (outerRadius d y0 p) r ^ 3 * TerminalStress.taperSlopeFactor d (edgeCoordinate (outerRadius d y0 p) r)

theorem NavierStokes.TerminalEdgeFactor.radialTaper_contDiffAt (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : ContDiffAt ℝ (↑⊤) (radialTaper d y0 p) r

theorem NavierStokes.TerminalEdgeFactor.radialTaper_deriv (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : deriv (radialTaper d y0 p) r = 2 / r * (FlatCutoff.edge 4 (edgeCoordinate (outerRadius d y0 p) r) / edgeCoordinate (outerRadius d y0 p) r ^ 3 * TerminalStress.taperSlopeFactor d (edgeCoordinate (outerRadius d y0 p) r))

theorem NavierStokes.TerminalEdgeFactor.radialTaper_plateau (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : radialTaper d y0 p =ᶠ[Filter.atTop] fun (x : ℝ) => 1

noncomputable def NavierStokes.TerminalEdgeFactor.boundaryCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Boundary coefficient, given by (2 * carrier C d y0 y / radius d y0 y) * taperSlopeFactor d y.2.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.timeCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Time coefficient, given by `(radius d y0 y ^ 3 * carrier C d y0 y / (2 * denominator d y.1))

• taperSlopeFactor d y.2`.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.correctionCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Correction coefficient, given by (radius d y0 y * carrier C d y0 y - radius d y0 y ^ 2 * carrierRadial C d y0 y) * taperSlopeFactor d y.2.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.boundaryCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (boundaryCoefficient C d y0)

theorem NavierStokes.TerminalEdgeFactor.timeCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (timeCoefficient C d y0)

theorem NavierStokes.TerminalEdgeFactor.correctionCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (correctionCoefficient C d y0)

theorem NavierStokes.TerminalEdgeFactor.carrier_at_radius (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : carrier C d y0 (p, edgeCoordinate (outerRadius d y0 p) r) = TerminalStress.heatAmplitude C (1 + d.h) (timeOf p) r

theorem NavierStokes.TerminalEdgeFactor.carrierRadial_at_radius (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : carrierRadial C d y0 (p, edgeCoordinate (outerRadius d y0 p) r) = deriv (TerminalStress.heatAmplitude C (1 + d.h) (timeOf p)) r

theorem NavierStokes.TerminalEdgeFactor.time_weight_eq_density (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : r ^ 2 * TerminalStress.timeResidual C d.h (logTaper d y0) (timeOf p) p.2 r = radialFlatDensity 4 3 (fun (v : ℝ) => timeCoefficient C d y0 (p, v)) (outerRadius d y0 p) r

theorem NavierStokes.TerminalEdgeFactor.correction_eq_density (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : TerminalStress.correction (TerminalStress.heatAmplitude C (1 + d.h) (timeOf p)) (radialTaper d y0 p) r = radialFlatDensity 4 3 (fun (v : ℝ) => correctionCoefficient C d y0 (p, v)) (outerRadius d y0 p) r

theorem NavierStokes.TerminalEdgeFactor.time_weight_integrable (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * TerminalStress.timeResidual C d.h (logTaper d y0) (timeOf p) p.2 u) (Set.Ioi r) MeasureTheory.volume

theorem NavierStokes.TerminalEdgeFactor.correction_integrable (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : MeasureTheory.IntegrableOn (TerminalStress.correction (TerminalStress.heatAmplitude C (1 + d.h) (timeOf p)) (radialTaper d y0 p)) (Set.Ioi r) MeasureTheory.volume

theorem NavierStokes.TerminalEdgeFactor.time_weight_integral (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ∫ (u : ℝ) in Set.Ioi (radius d y0 y), u ^ 2 * TerminalStress.timeResidual C d.h (logTaper d y0) (timeOf y.1) y.1.2 u = ParametricFlatFactor.primitive 4 3 (timeCoefficient C d y0) y

theorem NavierStokes.TerminalEdgeFactor.correction_integral (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ∫ (u : ℝ) in Set.Ioi (radius d y0 y), TerminalStress.correction (TerminalStress.heatAmplitude C (1 + d.h) (timeOf y.1)) (radialTaper d y0 y.1) u = ParametricFlatFactor.primitive 4 3 (correctionCoefficient C d y0) y

theorem NavierStokes.TerminalEdgeFactor.viscous_weight_integrable (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {r : ℝ} (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * TerminalStress.viscousResidual (TerminalStress.heatAmplitude C (1 + d.h) (timeOf p)) (radialTaper d y0 p) u) (Set.Ioi r) MeasureTheory.volume

noncomputable def NavierStokes.TerminalEdgeFactor.angularStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Angular stress, given by terminalStress C d.h (logTaper d y0) (timeOf y.1) y.1.2 (radius d y0 y).

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.angularFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Angular factor, constructed using boundaryCoefficient.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.angularFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (angularFactor C d y0)

theorem NavierStokes.TerminalEdgeFactor.angularStress_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : angularStress C d y0 y = FlatCutoff.edge 4 y.2 / y.2 ^ 3 * angularFactor C d y0 y

The leading angular stress itself, with all backward-integral hypotheses proved for the actual heat carrier and actual outgoing taper.

theorem NavierStokes.TerminalEdgeFactor.angularFactor_zero (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : angularFactor C d y0 (p, 0) = 2 * carrier C d y0 (p, 0) / radius d y0 (p, 0) * TerminalStress.taperSlopeFactor d 0

theorem NavierStokes.TerminalEdgeFactor.angularFactor_zero_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : 0 < angularFactor C d y0 (p, 0)

theorem NavierStokes.TerminalEdgeFactor.angularFactor_eventually_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : ∀ᶠ (y : EdgeParam × ℝ) in nhds (p, 0), 0 < angularFactor C d y0 y

theorem NavierStokes.TerminalEdgeFactor.angularStress_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (angularStress C d y0)

theorem NavierStokes.TerminalEdgeFactor.angularStress_normalized (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {δ : ℝ} (hδ : 0 < δ) : angularStress C d y0 (p, δ) / (Real.exp (-4 / δ ^ 2) / δ ^ 3) = angularFactor C d y0 (p, δ)

noncomputable def NavierStokes.TerminalEdgeFactor.logCoordinate (S s : ℝ) : ℝ

The same edge coordinate in the regular radial variable s=r²/2.

Equations

• NavierStokes.TerminalEdgeFactor.logCoordinate S s = NavierStokes.TerminalEdgeFactor.edgeCoordinate S s / 2

theorem NavierStokes.TerminalEdgeFactor.logCoordinate_hasDerivAt {S s : ℝ} (hS : 0 < S) (hs : 0 < s) : HasDerivAt (logCoordinate S) (-1 / s) s

theorem NavierStokes.TerminalEdgeFactor.logCoordinate_nonpos {S s : ℝ} (hS : 0 < S) (hSs : S ≤ s) : logCoordinate S s ≤ 0

noncomputable def NavierStokes.TerminalEdgeFactor.outerS (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : ℝ

Outer S, given by chartQ d p * Real.exp (y0 + 3).

Equations

• NavierStokes.TerminalEdgeFactor.outerS d y0 p = NavierStokes.TerminalEdgeFactor.chartQ d p * Real.exp (y0 + 3)

theorem NavierStokes.TerminalEdgeFactor.outerS_pos (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) : 0 < outerS d y0 p

theorem NavierStokes.TerminalEdgeFactor.radialS_eq (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : radius d y0 y ^ 2 / 2 = outerS d y0 y.1 * Real.exp (-y.2)

theorem NavierStokes.TerminalEdgeFactor.radialS_logCoordinate (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {s : ℝ} (hs : 0 < s) : radius d y0 (p, logCoordinate (outerS d y0 p) s) ^ 2 / 2 = s

theorem NavierStokes.TerminalEdgeFactor.logCoordinate_radialS (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : logCoordinate (outerS d y0 y.1) (radius d y0 y ^ 2 / 2) = y.2

theorem NavierStokes.TerminalEdgeFactor.physical_logX_s (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {s : ℝ} (hs : 0 < s) : Real.log (s / chartQ d p) = y0 + 3 - logCoordinate (outerS d y0 p) s

theorem NavierStokes.TerminalEdgeFactor.carrier_at_s (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {s : ℝ} (hs : 0 < s) : carrier C d y0 (p, logCoordinate (outerS d y0 p) s) = TerminalStress.physicalHeat C (1 + d.h) (timeOf p, s, p.2)

noncomputable def NavierStokes.TerminalEdgeFactor.scalarFlatDensity (c : ℝ) (j : ℕ) (a : ℝ → ℝ) (S s : ℝ) : ℝ

Scalar flat density, given by (1 / s) * FlatPrimitive.integrand c j a (logCoordinate S s).

Equations

• NavierStokes.TerminalEdgeFactor.scalarFlatDensity c j a S s = 1 / s * NavierStokes.FlatPrimitive.integrand c j a (NavierStokes.TerminalEdgeFactor.logCoordinate S s)

theorem NavierStokes.TerminalEdgeFactor.scalarFlatDensity_integrable {c S s : ℝ} (hc : 0 < c) (hS : 0 < S) (hs : 0 < s) (j : ℕ) {a : ℝ → ℝ} (ha : Continuous a) : MeasureTheory.IntegrableOn (scalarFlatDensity c j a S) (Set.Ioi s) MeasureTheory.volume

theorem NavierStokes.TerminalEdgeFactor.scalarFlatDensity_integral {c S s : ℝ} (hc : 0 < c) (hS : 0 < S) (hs : 0 < s) (j : ℕ) {a : ℝ → ℝ} (ha : Continuous a) : ∫ (u : ℝ) in Set.Ioi s, scalarFlatDensity c j a S u = FlatPrimitive.primitive c j a (logCoordinate S s)

noncomputable def NavierStokes.TerminalEdgeFactor.chi (d : OutgoingTail.TailData) (p : EdgeParam) : ℝ

Chi, given by 2 * chartEta d p / (chartQ d p ^ CoordinateAlgebra.D d.h * CoordinateAlgebra.L d.h (chartEta d p)).

Equations

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

theorem NavierStokes.TerminalEdgeFactor.chartL_pos (d : OutgoingTail.TailData) (p : EdgeParam) : 0 < CoordinateAlgebra.L d.h (chartEta d p)

theorem NavierStokes.TerminalEdgeFactor.chi_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (chi d)

theorem NavierStokes.TerminalEdgeFactor.chi_eq_logScale (d : OutgoingTail.TailData) (p : EdgeParam) : chi d p = CoordinateAlgebra.qAxial (chartQ d p) d.h (chartEta d p) / chartQ d p

noncomputable def NavierStokes.TerminalEdgeFactor.pressureCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Pressure coefficient, given by carrier C d y0 y ^ 2 * tailShape d (3 - y.2) * taperSlopeFactor d y.2.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.pressureCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (pressureCoefficient C d y0)

noncomputable def NavierStokes.TerminalEdgeFactor.pressureFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Pressure factor, given by chi d y.1 * ParametricFlatFactor.factor 4 3 (pressureCoefficient C d y0) y.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.pressureFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (pressureFactor C d y0)

noncomputable def NavierStokes.TerminalEdgeFactor.axialCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Axial coefficient, given by (radius d y0 y ^ 2 / 2) * pressureFactor C d y0 y.

Equations

• NavierStokes.TerminalEdgeFactor.axialCoefficient C d y0 y = NavierStokes.TerminalEdgeFactor.radius d y0 y ^ 2 / 2 * NavierStokes.TerminalEdgeFactor.pressureFactor C d y0 y

theorem NavierStokes.TerminalEdgeFactor.axialCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (axialCoefficient C d y0)

noncomputable def NavierStokes.TerminalEdgeFactor.axialFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

Axial factor, given by ParametricFlatFactor.factor 4 0 (axialCoefficient C d y0) y / radius d y0 y.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.axialFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (axialFactor C d y0)

noncomputable def NavierStokes.TerminalEdgeFactor.pressureGradient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

The actual canonical pressure gradient on the physical chart.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.axialStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ

The actual axial backward stress, written in the regular radius s=r²/2.

Equations

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

A profile chart including both endpoints η = ±1

These expressions use the actual heat profile on |η| ≤ 1. Its proven smooth extension and a positive extension of L supply coefficients on a neighborhood of that closed interval. No value of the implicit coordinates at zero backward time is used.

noncomputable def NavierStokes.TerminalEdgeFactor.positiveExtension (m x : ℝ) : ℝ

Positive extension, given by m / 2 + (x - m / 2) * OutgoingSchedule.sigma ((x - m / 2) / (m / 2)).

Equations

• NavierStokes.TerminalEdgeFactor.positiveExtension m x = m / 2 + (x - m / 2) * NavierStokes.OutgoingSchedule.sigma ((x - m / 2) / (m / 2))

theorem NavierStokes.TerminalEdgeFactor.positiveExtension_contDiff (m : ℝ) : ContDiff ℝ (↑⊤) (positiveExtension m)

theorem NavierStokes.TerminalEdgeFactor.positiveExtension_pos {m : ℝ} (hm : 0 < m) (x : ℝ) : 0 < positiveExtension m x

theorem NavierStokes.TerminalEdgeFactor.positiveExtension_eq {m x : ℝ} (hm : 0 < m) (hx : m ≤ x) : positiveExtension m x = x

noncomputable def NavierStokes.TerminalEdgeFactor.profileL (d : OutgoingTail.TailData) (η : ℝ) : ℝ

Profile L, given by positiveExtension (1 - 2 * d.h) (CoordinateAlgebra.L d.h η).

Equations

• NavierStokes.TerminalEdgeFactor.profileL d η = NavierStokes.TerminalEdgeFactor.positiveExtension (1 - 2 * d.h) (NavierStokes.CoordinateAlgebra.L d.h η)

theorem NavierStokes.TerminalEdgeFactor.profileL_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (profileL d)

theorem NavierStokes.TerminalEdgeFactor.profileL_pos (d : OutgoingTail.TailData) (η : ℝ) : 0 < profileL d η

theorem NavierStokes.TerminalEdgeFactor.profileL_eq (d : OutgoingTail.TailData) {η : ℝ} (hη : η ^ 2 ≤ 1) : profileL d η = CoordinateAlgebra.L d.h η

theorem NavierStokes.TerminalEdgeFactor.eta_sq_le_one {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : η ^ 2 ≤ 1

noncomputable def NavierStokes.TerminalEdgeFactor.profileS (y0 x : ℝ) : ℝ

Profile S, given by Real.exp (y0 + 3 - x).

Equations

• NavierStokes.TerminalEdgeFactor.profileS y0 x = Real.exp (y0 + 3 - x)

noncomputable def NavierStokes.TerminalEdgeFactor.profileRadius (y0 x : ℝ) : ℝ

Profile radius, given by Real.sqrt (2 * Real.exp (y0 + 3)) * Real.exp (-x / 2).

Equations

• NavierStokes.TerminalEdgeFactor.profileRadius y0 x = √(2 * Real.exp (y0 + 3)) * Real.exp (-x / 2)

noncomputable def NavierStokes.TerminalEdgeFactor.profileZ (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile Z, given by 2 * (1 - y.1 ^ 2) / profileS y0 y.2.

Equations

• NavierStokes.TerminalEdgeFactor.profileZ y0 y = 2 * (1 - y.1 ^ 2) / NavierStokes.TerminalEdgeFactor.profileS y0 y.2

theorem NavierStokes.TerminalEdgeFactor.profileS_pos (y0 x : ℝ) : 0 < profileS y0 x

theorem NavierStokes.TerminalEdgeFactor.profileS_contDiff (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileS y0)

theorem NavierStokes.TerminalEdgeFactor.profileRadius_pos (y0 x : ℝ) : 0 < profileRadius y0 x

theorem NavierStokes.TerminalEdgeFactor.profileRadius_contDiff (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileRadius y0)

theorem NavierStokes.TerminalEdgeFactor.profileRadius_square (y0 x : ℝ) : profileRadius y0 x ^ 2 = 2 * profileS y0 x

theorem NavierStokes.TerminalEdgeFactor.profileZ_contDiff (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileZ y0)

theorem NavierStokes.TerminalEdgeFactor.profileZ_nonneg (y0 : ℝ) {y : ℝ × ℝ} (hη : y.1 ^ 2 ≤ 1) : 0 ≤ profileZ y0 y

noncomputable def NavierStokes.TerminalEdgeFactor.profileCarrier (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile carrier, given by C * (profileS y0 y.2) ^ RadialHeatProfile.spatialExponent (1 + d.h) * HeatProfileExtension.extension (1 + d.h) (profileZ y0 y).

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.profileCarrierRadial (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile carrier radial, constructed using C.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profileCarrier_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileCarrier C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileCarrierRadial_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileCarrierRadial C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileCarrier_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {y : ℝ × ℝ} (hη : y.1 ^ 2 ≤ 1) : 0 < profileCarrier C d y0 y

noncomputable def NavierStokes.TerminalEdgeFactor.profileChi (d : OutgoingTail.TailData) (η : ℝ) : ℝ

Profile chi, given by 2 * η / profileL d η.

Equations

• NavierStokes.TerminalEdgeFactor.profileChi d η = 2 * η / NavierStokes.TerminalEdgeFactor.profileL d η

theorem NavierStokes.TerminalEdgeFactor.profileChi_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (profileChi d)

noncomputable def NavierStokes.TerminalEdgeFactor.profileBoundaryCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile boundary coefficient, given by `(2 * profileCarrier C d y0 y / profileRadius y0 y.2)

• taperSlopeFactor d y.2`.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.profileTimeCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile time coefficient, given by `(profileRadius y0 y.2 ^ 3 * profileCarrier C d y0 y / (2

• profileL d y.1)) * taperSlopeFactor d y.2`.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.profileCorrectionCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile correction coefficient as an element of ℝ.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profileBoundaryCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileBoundaryCoefficient C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileTimeCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileTimeCoefficient C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileCorrectionCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileCorrectionCoefficient C d y0)

noncomputable def NavierStokes.TerminalEdgeFactor.profileAngularFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile angular factor, constructed using profileBoundaryCoefficient.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.profileAngularStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

The boundary term and the two actual terminal primitives in profile coordinates.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profileAngularFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileAngularFactor C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileAngularStress_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profileAngularStress C d y0 y = FlatCutoff.edge 4 y.2 / y.2 ^ 3 * profileAngularFactor C d y0 y

theorem NavierStokes.TerminalEdgeFactor.profileAngularFactor_zero (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) : profileAngularFactor C d y0 (η, 0) = 2 * profileCarrier C d y0 (η, 0) / profileRadius y0 0 * TerminalStress.taperSlopeFactor d 0

theorem NavierStokes.TerminalEdgeFactor.profileAngularFactor_zero_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : 0 < profileAngularFactor C d y0 (η, 0)

noncomputable def NavierStokes.TerminalEdgeFactor.profilePressureCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile pressure coefficient, given by `profileCarrier C d y0 y ^ 2 * tailShape d (3 - y.2)

• taperSlopeFactor d y.2`.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profilePressureCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profilePressureCoefficient C d y0)

noncomputable def NavierStokes.TerminalEdgeFactor.profilePressureFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile pressure factor, given by profileChi d y.1 * ParametricFlatFactor.factor 4 3 (profilePressureCoefficient C d y0) y.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.profilePressureGradient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

The first genuine terminal primitive, before any factorization.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profilePressureFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profilePressureFactor C d y0)

theorem NavierStokes.TerminalEdgeFactor.scale_three (c x : ℝ) : FlatPrimitive.scale c 3 x = FlatCutoff.edge c x

theorem NavierStokes.TerminalEdgeFactor.profilePressureGradient_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profilePressureGradient C d y0 y = FlatCutoff.edge 4 y.2 * profilePressureFactor C d y0 y

noncomputable def NavierStokes.TerminalEdgeFactor.profileAxialCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile axial coefficient, given by profileS y0 y.2 * profilePressureFactor C d y0 y.

Equations

• NavierStokes.TerminalEdgeFactor.profileAxialCoefficient C d y0 y = NavierStokes.TerminalEdgeFactor.profileS y0 y.2 * NavierStokes.TerminalEdgeFactor.profilePressureFactor C d y0 y

noncomputable def NavierStokes.TerminalEdgeFactor.profileAxialFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile axial factor, given by ParametricFlatFactor.factor 4 0 (profileAxialCoefficient C d y0) y / profileRadius y0 y.2.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.profileAxialStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

The second terminal primitive is the integral of the first one, with the exact Jacobian s = exp(Y-δ) of the regular radial coordinate.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profileAxialCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileAxialCoefficient C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileAxialFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileAxialFactor C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileAxialStress_eq_primitive (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profileAxialStress C d y0 y = ParametricFlatFactor.primitive 4 0 (profileAxialCoefficient C d y0) y / profileRadius y0 y.2

theorem NavierStokes.TerminalEdgeFactor.profileAxialStress_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profileAxialStress C d y0 y = FlatCutoff.edge 4 y.2 * y.2 ^ 3 * profileAxialFactor C d y0 y

Identification of both physical pressure primitives

theorem NavierStokes.TerminalEdgeFactor.pressure_density_eq (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {s : ℝ} (hs : 0 < s) : TerminalStress.physicalHeat C (1 + d.h) (timeOf p, s, p.2) ^ 2 * OutgoingTail.tailShape d (Real.log (s / chartQ d p) - y0) * OutgoingTail.tailShapeDeriv d (Real.log (s / chartQ d p) - y0) / s = scalarFlatDensity 4 3 (fun (v : ℝ) => pressureCoefficient C d y0 (p, v)) (outerS d y0 p) s

theorem NavierStokes.TerminalEdgeFactor.pressureGradient_eq_primitive (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : pressureGradient C d y0 y = chi d y.1 * ParametricFlatFactor.primitive 4 3 (pressureCoefficient C d y0) y

theorem NavierStokes.TerminalEdgeFactor.pressureGradient_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : pressureGradient C d y0 y = FlatCutoff.edge 4 y.2 * pressureFactor C d y0 y

theorem NavierStokes.TerminalEdgeFactor.pressureGradient_at_s (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {s : ℝ} (hs : 0 < s) : SimilarityProfile.partialZ (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C d.h (logTaper d y0))) (timeOf p, s, p.2) = FlatCutoff.edge 4 (logCoordinate (outerS d y0 p) s) * pressureFactor C d y0 (p, logCoordinate (outerS d y0 p) s)

theorem NavierStokes.TerminalEdgeFactor.axial_density_eq (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : EdgeParam) {s : ℝ} (hs : 0 < s) : SimilarityProfile.partialZ (TerminalStress.canonicalPressure (TerminalStress.swirlCoefficient C d.h (logTaper d y0))) (timeOf p, s, p.2) = scalarFlatDensity 4 0 (fun (v : ℝ) => axialCoefficient C d y0 (p, v)) (outerS d y0 p) s

theorem NavierStokes.TerminalEdgeFactor.axialStress_eq_primitive (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : axialStress C d y0 y = ParametricFlatFactor.primitive 4 0 (axialCoefficient C d y0) y / radius d y0 y

theorem NavierStokes.TerminalEdgeFactor.axialStress_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : axialStress C d y0 y = FlatCutoff.edge 4 y.2 * y.2 ^ 3 * axialFactor C d y0 y

Agreement with the physical section away from the endpoints

noncomputable def NavierStokes.TerminalEdgeFactor.normalizedParam (η : ℝ) : EdgeParam

Normalized param, given by (Real.log (1 - η ^ 2), η).

Equations

• NavierStokes.TerminalEdgeFactor.normalizedParam η = (Real.log (1 - η ^ 2), η)

theorem NavierStokes.TerminalEdgeFactor.timeOf_normalizedParam {η : ℝ} (hη : η ^ 2 < 1) : timeOf (normalizedParam η) = η ^ 2

theorem NavierStokes.TerminalEdgeFactor.chartQ_normalizedParam (d : OutgoingTail.TailData) {η : ℝ} (hη : η ^ 2 < 1) : chartQ d (normalizedParam η) = 1

theorem NavierStokes.TerminalEdgeFactor.chartEta_normalizedParam (d : OutgoingTail.TailData) {η : ℝ} (hη : η ^ 2 < 1) : chartEta d (normalizedParam η) = η

theorem NavierStokes.TerminalEdgeFactor.radius_normalizedParam (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : radius d y0 (normalizedParam η, x) = profileRadius y0 x

theorem NavierStokes.TerminalEdgeFactor.radialS_normalizedParam (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : radius d y0 (normalizedParam η, x) ^ 2 / 2 = profileS y0 x

theorem NavierStokes.TerminalEdgeFactor.carrier_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : carrier C d y0 (normalizedParam η, x) = profileCarrier C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.carrierRadial_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : carrierRadial C d y0 (normalizedParam η, x) = profileCarrierRadial C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.denominator_normalizedParam (d : OutgoingTail.TailData) {η : ℝ} (hη : η ^ 2 < 1) : denominator d (normalizedParam η) = profileL d η

theorem NavierStokes.TerminalEdgeFactor.chi_normalizedParam (d : OutgoingTail.TailData) {η : ℝ} (hη : η ^ 2 < 1) : chi d (normalizedParam η) = profileChi d η

theorem NavierStokes.TerminalEdgeFactor.boundaryCoefficient_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : boundaryCoefficient C d y0 (normalizedParam η, x) = profileBoundaryCoefficient C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.timeCoefficient_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : timeCoefficient C d y0 (normalizedParam η, x) = profileTimeCoefficient C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.correctionCoefficient_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : correctionCoefficient C d y0 (normalizedParam η, x) = profileCorrectionCoefficient C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.pressureCoefficient_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : pressureCoefficient C d y0 (normalizedParam η, x) = profilePressureCoefficient C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.factor_congr_slice {P : Type u_1} {Q : Type u_2} (c : ℝ) (j : ℕ) (b : P × ℝ → ℝ) (a : Q × ℝ → ℝ) (p : P) (q : Q) (x : ℝ) (he : ∀ (u : ℝ), b (p, u) = a (q, u)) : ParametricFlatFactor.factor c j b (p, x) = ParametricFlatFactor.factor c j a (q, x)

theorem NavierStokes.TerminalEdgeFactor.angularFactor_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : angularFactor C d y0 (normalizedParam η, x) = profileAngularFactor C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.pressureFactor_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : pressureFactor C d y0 (normalizedParam η, x) = profilePressureFactor C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.axialCoefficient_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : axialCoefficient C d y0 (normalizedParam η, x) = profileAxialCoefficient C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.axialFactor_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : axialFactor C d y0 (normalizedParam η, x) = profileAxialFactor C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.angularStress_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : angularStress C d y0 (normalizedParam η, x) = profileAngularStress C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.pressureGradient_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : pressureGradient C d y0 (normalizedParam η, x) = profilePressureGradient C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.axialStress_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : axialStress C d y0 (normalizedParam η, x) = profileAxialStress C d y0 (η, x)

Full profile stress, all jets, and the edge direction

noncomputable def NavierStokes.TerminalEdgeFactor.profileStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ × ℝ

Profile stress, given by (profileAngularStress C d y0 y, profileAxialStress C d y0 y).

Equations

• NavierStokes.TerminalEdgeFactor.profileStress C d y0 y = (NavierStokes.TerminalEdgeFactor.profileAngularStress C d y0 y, NavierStokes.TerminalEdgeFactor.profileAxialStress C d y0 y)

noncomputable def NavierStokes.TerminalEdgeFactor.profileStressFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ × ℝ

Profile stress factor, given by (profileAngularFactor C d y0 y, y.2 ^ 6 * profileAxialFactor C d y0 y).

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profileStressFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileStressFactor C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileStress_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profileStress C d y0 y = (FlatCutoff.edge 4 y.2 / y.2 ^ 3) • profileStressFactor C d y0 y

theorem NavierStokes.TerminalEdgeFactor.profileStress_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileStress C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileStressFactor_zero (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) : profileStressFactor C d y0 (η, 0) = (profileAngularFactor C d y0 (η, 0), 0)

theorem NavierStokes.TerminalEdgeFactor.profileStressFactor_zero_ne {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : profileStressFactor C d y0 (η, 0) ≠ 0

theorem NavierStokes.TerminalEdgeFactor.profileStress_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (n : ℕ) {b : ℝ} (hb : 0 < b) : ∃ (A : ℝ), 0 < A ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ η ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x ≤ b → ‖iteratedFDeriv ℝ i (profileStress C d y0) (η, x)‖ ≤ A * FlatCutoff.edge 4 x / x ^ N

Actual full tensors, uniformly through both endpoints of the profile interval.

theorem NavierStokes.TerminalEdgeFactor.profileAngularStress_edge_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (n : ℕ) (η : ℝ) : iteratedFDeriv ℝ n (profileAngularStress C d y0) (η, 0) = 0

theorem NavierStokes.TerminalEdgeFactor.profileAxialStress_edge_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (n : ℕ) (η : ℝ) : iteratedFDeriv ℝ n (profileAxialStress C d y0) (η, 0) = 0

noncomputable def NavierStokes.TerminalEdgeFactor.profileTilt (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile tilt, given by y.2 ^ 6 * profileAxialFactor C d y0 y / profileAngularFactor C d y0 y.

Equations

• NavierStokes.TerminalEdgeFactor.profileTilt C d y0 y = y.2 ^ 6 * NavierStokes.TerminalEdgeFactor.profileAxialFactor C d y0 y / NavierStokes.TerminalEdgeFactor.profileAngularFactor C d y0 y

theorem NavierStokes.TerminalEdgeFactor.profileTilt_eq_ratio (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) {x : ℝ} (hx : 0 < x) : profileAxialStress C d y0 (η, x) / profileAngularStress C d y0 (η, x) = profileTilt C d y0 (η, x)

theorem NavierStokes.TerminalEdgeFactor.profileTilt_zero (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) : profileTilt C d y0 (η, 0) = 0

theorem NavierStokes.TerminalEdgeFactor.profileTilt_contDiffAt {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : ContDiffAt ℝ (↑⊤) (profileTilt C d y0) (η, 0)

theorem NavierStokes.TerminalEdgeFactor.profileTilt_tendsto_zero {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : Filter.Tendsto (profileTilt C d y0) (nhds (η, 0)) (nhds 0)

noncomputable def NavierStokes.TerminalEdgeFactor.profileSpeed (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

The actual velocity shear ratio for the terminal product K f_o.

Equations

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

theorem NavierStokes.TerminalEdgeFactor.profileSpeed_contDiffAt_of_ne (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {y : ℝ × ℝ} (hK : profileCarrier C d y0 y ≠ 0) : ContDiffAt ℝ (↑⊤) (profileSpeed C d y0) y

theorem NavierStokes.TerminalEdgeFactor.profileSpeed_contDiffAt {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {y : ℝ × ℝ} (hη : y.1 ^ 2 ≤ 1) : ContDiffAt ℝ (↑⊤) (profileSpeed C d y0) y

noncomputable def NavierStokes.TerminalEdgeFactor.profileDomain (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : Set (ℝ × ℝ)

Profile domain, given by {y | profileCarrier C d y0 y ≠ 0}.

Equations

• NavierStokes.TerminalEdgeFactor.profileDomain C d y0 = {y : ℝ × ℝ | NavierStokes.TerminalEdgeFactor.profileCarrier C d y0 y ≠ 0}

theorem NavierStokes.TerminalEdgeFactor.profileDomain_open (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : IsOpen (profileDomain C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileDomain_contains_closed {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) : Set.Icc (-1) 1 ×ˢ Set.univ ⊆ profileDomain C d y0

theorem NavierStokes.TerminalEdgeFactor.profileSpeed_contDiffOn (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiffOn ℝ (↑⊤) (profileSpeed C d y0) (profileDomain C d y0)

theorem NavierStokes.TerminalEdgeFactor.extended_heat_slope (d : OutgoingTail.TailData) {z : ℝ} (hz : 0 ≤ z) : -z * deriv (HeatProfileExtension.extension (1 + d.h)) z < d.h * HeatProfileExtension.extension (1 + d.h) z

theorem NavierStokes.TerminalEdgeFactor.profileCarrier_radial_gap {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {y : ℝ × ℝ} (hη : y.1 ^ 2 ≤ 1) : profileRadius y0 y.2 * profileCarrierRadial C d y0 y + profileCarrier C d y0 y < 0

theorem NavierStokes.TerminalEdgeFactor.profileSpeed_zero_gt_two {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : 2 < profileSpeed C d y0 (η, 0)

noncomputable def NavierStokes.TerminalEdgeFactor.profileConeGap (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile cone gap, given by 2 - (profileSpeed C d y0 y - 2) * profileTilt C d y0 y ^ 2.

Equations

• NavierStokes.TerminalEdgeFactor.profileConeGap C d y0 y = 2 - (NavierStokes.TerminalEdgeFactor.profileSpeed C d y0 y - 2) * NavierStokes.TerminalEdgeFactor.profileTilt C d y0 y ^ 2

theorem NavierStokes.TerminalEdgeFactor.profileConeGap_zero (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) : profileConeGap C d y0 (η, 0) = 2

theorem NavierStokes.TerminalEdgeFactor.compact_positive_collar {E : Type u_1} [NormedAddCommGroup E] {K : Set E} (hK : IsCompact K) {f : E × ℝ → ℝ} (hf : ∀ p ∈ K, ContinuousAt f (p, 0)) (hpos : ∀ p ∈ K, 0 < f (p, 0)) : ∃ (ε : ℝ) (m : ℝ), 0 < ε ∧ 0 < m ∧ ∀ p ∈ K, ∀ (x : ℝ), |x| < ε → m ≤ f (p, x)

theorem NavierStokes.TerminalEdgeFactor.profile_uniform_cone {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) : ∃ (ε : ℝ) (m : ℝ), 0 < ε ∧ 0 < m ∧ ∀ η ∈ Set.Icc (-1) 1, ∀ (x : ℝ), |x| < ε → m ≤ profileAngularFactor C d y0 (η, x) ∧ m ≤ profileSpeed C d y0 (η, x) - 2 ∧ m ≤ profileConeGap C d y0 (η, x)

One strict relative cone margin on a collar, uniformly for -1 ≤ η ≤ 1. The shear is the finite, actual terminal velocity shear; its value is proved strictly larger than two on the boundary.

The shear formula is the derivative of the actual profile velocity

noncomputable def NavierStokes.TerminalEdgeFactor.profileAngularVelocity (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile angular velocity, given by profileCarrier C d y0 y * tailShape d (3 - y.2).

Equations

• NavierStokes.TerminalEdgeFactor.profileAngularVelocity C d y0 y = NavierStokes.TerminalEdgeFactor.profileCarrier C d y0 y * NavierStokes.OutgoingTail.tailShape d (3 - y.2)

theorem NavierStokes.TerminalEdgeFactor.profileAngularVelocity_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileAngularVelocity C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileS_hasDerivAt (y0 x : ℝ) : HasDerivAt (profileS y0) (-profileS y0 x) x

theorem NavierStokes.TerminalEdgeFactor.profileZ_hasDerivAt (y0 η x : ℝ) : HasDerivAt (fun (u : ℝ) => profileZ y0 (η, u)) (profileZ y0 (η, x)) x

theorem NavierStokes.TerminalEdgeFactor.profileCarrier_hasDerivAt_edge (C : ℝ) (d : OutgoingTail.TailData) (y0 η x : ℝ) : HasDerivAt (fun (u : ℝ) => profileCarrier C d y0 (η, u)) (-(profileRadius y0 x * profileCarrierRadial C d y0 (η, x)) / 2) x

theorem NavierStokes.TerminalEdgeFactor.profileAngularVelocity_hasDerivAt_edge (C : ℝ) (d : OutgoingTail.TailData) (y0 η x : ℝ) : HasDerivAt (fun (u : ℝ) => profileAngularVelocity C d y0 (η, u)) (-(profileRadius y0 x * profileCarrierRadial C d y0 (η, x)) / 2 * OutgoingTail.tailShape d (3 - x) - profileCarrier C d y0 (η, x) * OutgoingTail.tailShapeDeriv d (3 - x)) x

theorem NavierStokes.TerminalEdgeFactor.profileSpeed_eq_log_deriv {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 η x : ℝ) (hη : η ∈ Set.Icc (-1) 1) : profileSpeed C d y0 (η, x) = 1 + 2 * deriv (fun (u : ℝ) => profileAngularVelocity C d y0 (η, u)) x / profileAngularVelocity C d y0 (η, x)

Since δ=Y-2 log r, 1+2 ∂δ log(K f_o) is exactly the radial shear 1-r ∂r(K f_o)/(K f_o). Here its logarithmic derivative is proved directly.

theorem NavierStokes.TerminalEdgeFactor.profile_relative_cone {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) : ∃ (ε : ℝ), 0 < ε ∧ ∀ η ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x < ε → 0 < profileAngularStress C d y0 (η, x) ∧ 2 < profileSpeed C d y0 (η, x) ∧ (profileSpeed C d y0 (η, x) - 2) * profileAxialStress C d y0 (η, x) ^ 2 < 2 * profileAngularStress C d y0 (η, x) ^ 2

The strict cone inequalities for the actual stress hold throughout one positive-width terminal collar, uniformly through the closed profile interval.

The same weighted estimates on compact physical parameter sets

noncomputable def NavierStokes.TerminalEdgeFactor.physicalStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ × ℝ

Physical stress, given by (angularStress C d y0 y, axialStress C d y0 y).

Equations

• NavierStokes.TerminalEdgeFactor.physicalStress C d y0 y = (NavierStokes.TerminalEdgeFactor.angularStress C d y0 y, NavierStokes.TerminalEdgeFactor.axialStress C d y0 y)

noncomputable def NavierStokes.TerminalEdgeFactor.physicalStressFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : ℝ × ℝ

Physical stress factor, given by (angularFactor C d y0 y, y.2 ^ 6 * axialFactor C d y0 y).

Equations

• NavierStokes.TerminalEdgeFactor.physicalStressFactor C d y0 y = (NavierStokes.TerminalEdgeFactor.angularFactor C d y0 y, y.2 ^ 6 * NavierStokes.TerminalEdgeFactor.axialFactor C d y0 y)

theorem NavierStokes.TerminalEdgeFactor.physicalStressFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (physicalStressFactor C d y0)

theorem NavierStokes.TerminalEdgeFactor.physicalStress_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : EdgeParam × ℝ) : physicalStress C d y0 y = (FlatCutoff.edge 4 y.2 / y.2 ^ 3) • physicalStressFactor C d y0 y

theorem NavierStokes.TerminalEdgeFactor.physicalStress_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {S : Set EdgeParam} (hS : IsCompact S) (n : ℕ) {b : ℝ} (hb : 0 < b) : ∃ (A : ℝ), 0 < A ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ p ∈ S, ∀ (x : ℝ), 0 < x → x ≤ b → ‖iteratedFDeriv ℝ i (physicalStress C d y0) (p, x)‖ ≤ A * FlatCutoff.edge 4 x / x ^ N

theorem NavierStokes.TerminalEdgeFactor.physicalStress_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (physicalStress C d y0)

theorem NavierStokes.TerminalEdgeFactor.profileStress_of_nonpos (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {y : ℝ × ℝ} (hy : y.2 ≤ 0) : profileStress C d y0 y = 0

theorem NavierStokes.TerminalEdgeFactor.physicalStress_of_nonpos (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {y : EdgeParam × ℝ} (hy : y.2 ≤ 0) : physicalStress C d y0 y = 0

theorem NavierStokes.TerminalEdgeFactor.physicalStress_normalizedParam (C : ℝ) (d : OutgoingTail.TailData) (y0 x : ℝ) {η : ℝ} (hη : η ^ 2 < 1) : physicalStress C d y0 (normalizedParam η, x) = profileStress C d y0 (η, x)

The genuine root-form cone on the terminal collar

noncomputable def NavierStokes.TerminalEdgeFactor.profileSwirlCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile swirl coefficient, given by profileAngularVelocity C d y0 y / profileRadius y0 y.2.

Equations

• NavierStokes.TerminalEdgeFactor.profileSwirlCoefficient C d y0 y = NavierStokes.TerminalEdgeFactor.profileAngularVelocity C d y0 y / NavierStokes.TerminalEdgeFactor.profileRadius y0 y.2

theorem NavierStokes.TerminalEdgeFactor.profileSwirlCoefficient_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {y : ℝ × ℝ} (hη : y.1 ∈ Set.Icc (-1) 1) : 0 < profileSwirlCoefficient C d y0 y

noncomputable def NavierStokes.TerminalEdgeFactor.profileP (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile P, given by profileSpeed C d y0 y + profileAngularStress C d y0 y / profileSwirlCoefficient C d y0 y.

Equations

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

noncomputable def NavierStokes.TerminalEdgeFactor.profileJ (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile J, given by profileAxialStress C d y0 y / profileSwirlCoefficient C d y0 y.

Equations

• NavierStokes.TerminalEdgeFactor.profileJ C d y0 y = NavierStokes.TerminalEdgeFactor.profileAxialStress C d y0 y / NavierStokes.TerminalEdgeFactor.profileSwirlCoefficient C d y0 y

theorem NavierStokes.TerminalEdgeFactor.profile_true_cone {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) : ∃ (ε : ℝ), 0 < ε ∧ ∀ η ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x < ε → 2 < profileP C d y0 (η, x) ∧ profileSpeed C d y0 (η, x) < ConeAlgebra.coneBound (profileP C d y0 (η, x)) (profileJ C d y0 (η, x))

Applying the exact true-cone equivalence to the actual terminal stress, with P-v=Tθ/F and J=Tz/F, rather than taking a large-amplitude limit.