Actual histories of the corrected outgoing fields

The first coordinate is the global logarithmic radius y, with normalized X = exp y. In particular smoothness here is not smoothness at the radial axis. Every history starts with the integral of the explicit ideal past and then integrates the same corrected angular field and the same axial field. The axial amplitude can be any smooth function of the parameter.

I and J omit the common physical factor sqrt 2. For arbitrary entrance radius XR, the physical factors are XR for M,S and XR * sqrt (2*XR) for I,J. These factors cancel from both normalized lags.

@[reducible, inline]

abbrev NavierStokes.OutgoingHistories.Point : Type

Point: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.OutgoingHistories.Point = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.OutgoingHistories.Field : Type

Field: an abbreviation for Point → ℝ.

Equations

• NavierStokes.OutgoingHistories.Field = (NavierStokes.OutgoingHistories.Point → ℝ)

@[reducible, inline]

noncomputable abbrev NavierStokes.OutgoingHistories.dY (F : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

D Y: an abbreviation for ProfileHistories.radialPartial.

Equations

• NavierStokes.OutgoingHistories.dY = NavierStokes.ProfileHistories.radialPartial

@[reducible, inline]

noncomputable abbrev NavierStokes.OutgoingHistories.dEta (F : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

D eta: an abbreviation for ProfileHistories.parameterPartial.

Equations

• NavierStokes.OutgoingHistories.dEta = NavierStokes.ProfileHistories.parameterPartial

noncomputable def NavierStokes.OutgoingHistories.logDomain : ProfileHistories.RadialDomain

The whole log-coordinate plane; this is not a radial domain at X=0.

Equations

• NavierStokes.OutgoingHistories.logDomain = { carrier := Set.univ, isOpen := NavierStokes.OutgoingHistories.logDomain._proof_2, scale_mem := NavierStokes.OutgoingHistories.logDomain._proof_1 }

theorem NavierStokes.OutgoingHistories.dY_hasDerivAt {f : Field} (hf : ContDiff ℝ (↑⊤) f) (p : Point) : HasDerivAt (fun (y : ℝ) => f (y, p.2)) (dY f p) p.1

theorem NavierStokes.OutgoingHistories.dEta_hasDerivAt {f : Field} (hf : ContDiff ℝ (↑⊤) f) (p : Point) : HasDerivAt (fun (eta : ℝ) => f (p.1, eta)) (dEta f p) p.2

theorem NavierStokes.OutgoingHistories.dY_eq_deriv {f : Field} (hf : ContDiff ℝ (↑⊤) f) (p : Point) : dY f p = deriv (fun (y : ℝ) => f (y, p.2)) p.1

theorem NavierStokes.OutgoingHistories.dEta_eq_deriv {f : Field} (hf : ContDiff ℝ (↑⊤) f) (p : Point) : dEta f p = deriv (fun (eta : ℝ) => f (p.1, eta)) p.2

theorem NavierStokes.OutgoingHistories.dY_smooth {f : Field} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (dY f)

theorem NavierStokes.OutgoingHistories.dEta_smooth {f : Field} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (dEta f)

noncomputable def NavierStokes.OutgoingHistories.history (initial : ℝ → ℝ) (f : Field) (p : Point) : ℝ

A fixed incoming integral plus a finite log-coordinate integral.

Equations

• NavierStokes.OutgoingHistories.history initial f p = initial p.2 + NavierStokes.ProfileHistories.primitive f p

theorem NavierStokes.OutgoingHistories.prefix_smooth {initial : ℝ → ℝ} {f : Field} (hi : ContDiff ℝ (↑⊤) initial) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (history initial f)

theorem NavierStokes.OutgoingHistories.prefix_hasDerivAt {initial : ℝ → ℝ} {f : Field} (hf : ContDiff ℝ (↑⊤) f) (p : Point) : HasDerivAt (fun (y : ℝ) => history initial f (y, p.2)) (f p) p.1

theorem NavierStokes.OutgoingHistories.dEta_prefix {initial : ℝ → ℝ} {f : Field} (hi : ContDiff ℝ (↑⊤) initial) (hf : ContDiff ℝ (↑⊤) f) (p : Point) : dEta (history initial f) p = deriv initial p.2 + ProfileHistories.primitive (dEta f) p

theorem NavierStokes.OutgoingHistories.dEta_prefix_hasDerivAt {initial : ℝ → ℝ} {f : Field} (hi : ContDiff ℝ (↑⊤) initial) (hf : ContDiff ℝ (↑⊤) f) (p : Point) : HasDerivAt (fun (y : ℝ) => dEta (history initial f) (y, p.2)) (dEta f p) p.1

theorem NavierStokes.OutgoingHistories.dEta_mul {f g : Field} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (p : Point) : dEta (fun (q : ProfileHistories.Point) => f q * g q) p = dEta f p * g p + f p * dEta g p

noncomputable def NavierStokes.OutgoingHistories.X (p : Point) : ℝ

X, given by Real.exp p.1.

Equations

• NavierStokes.OutgoingHistories.X p = Real.exp p.1

theorem NavierStokes.OutgoingHistories.X_pos (p : Point) : 0 < X p

theorem NavierStokes.OutgoingHistories.X_smooth : ContDiff ℝ (↑⊤) X

theorem NavierStokes.OutgoingHistories.X_hasDerivAt (p : Point) : HasDerivAt (fun (y : ℝ) => X (y, p.2)) (X p) p.1

theorem NavierStokes.OutgoingHistories.dEta_X (p : Point) : dEta X p = 0

noncomputable def NavierStokes.OutgoingHistories.E {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : Field

E, given by correctedAngular d w.coefficients.

Equations

• NavierStokes.OutgoingHistories.E w = NavierStokes.UniformAngularReset.correctedAngular d w.coefficients

noncomputable def NavierStokes.OutgoingHistories.U (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) : Field

U, given by axial d.core Amp.

Equations

• NavierStokes.OutgoingHistories.U d Amp = NavierStokes.OutgoingSchedule.axial d.core Amp

noncomputable def NavierStokes.OutgoingHistories.H {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : ℝ

H, given by Real.exp (p.1 / 2) * E w p.

Equations

• NavierStokes.OutgoingHistories.H w p = Real.exp (p.1 / 2) * NavierStokes.OutgoingHistories.E w p

noncomputable def NavierStokes.OutgoingHistories.massWeight (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (p : Point) : ℝ

Mass weight, given by X p * U d Amp p.

Equations

• NavierStokes.OutgoingHistories.massWeight d Amp p = NavierStokes.OutgoingHistories.X p * NavierStokes.OutgoingHistories.U d Amp p

noncomputable def NavierStokes.OutgoingHistories.angularWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : ℝ

Angular weight, given by X p * H w p.

Equations

• NavierStokes.OutgoingHistories.angularWeight w p = NavierStokes.OutgoingHistories.X p * NavierStokes.OutgoingHistories.H w p

noncomputable def NavierStokes.OutgoingHistories.transportWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Transport weight, given by X p * (U d Amp p * H w p).

Equations

• NavierStokes.OutgoingHistories.transportWeight w Amp p = NavierStokes.OutgoingHistories.X p * (NavierStokes.OutgoingHistories.U d Amp p * NavierStokes.OutgoingHistories.H w p)

noncomputable def NavierStokes.OutgoingHistories.energyDensity {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Energy density, given by U d Amp p ^ 2 - E w p ^ 2 / 2.

Equations

• NavierStokes.OutgoingHistories.energyDensity w Amp p = NavierStokes.OutgoingHistories.U d Amp p ^ 2 - NavierStokes.OutgoingHistories.E w p ^ 2 / 2

noncomputable def NavierStokes.OutgoingHistories.energyWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Energy weight, given by X p * energyDensity w Amp p.

Equations

• NavierStokes.OutgoingHistories.energyWeight w Amp p = NavierStokes.OutgoingHistories.X p * NavierStokes.OutgoingHistories.energyDensity w Amp p

noncomputable def NavierStokes.OutgoingHistories.pressureWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : ℝ

Pressure weight, given by E w p ^ 2 / 2.

Equations

• NavierStokes.OutgoingHistories.pressureWeight w p = NavierStokes.OutgoingHistories.E w p ^ 2 / 2

noncomputable def NavierStokes.OutgoingHistories.initialM (eta : ℝ) : ℝ

Initial M, given by 4 * eta.

Equations

• NavierStokes.OutgoingHistories.initialM eta = 4 * eta

noncomputable def NavierStokes.OutgoingHistories.initialI (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Initial I, given by (5 / 8) * d.core.P * shape eta.

Equations

• NavierStokes.OutgoingHistories.initialI d eta = 5 / 8 * d.core.P * NavierStokes.OutgoingSchedule.shape eta

noncomputable def NavierStokes.OutgoingHistories.initialJ (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Initial J, given by (5 / 2) * d.core.P * eta * shape eta.

Equations

• NavierStokes.OutgoingHistories.initialJ d eta = 5 / 2 * d.core.P * eta * NavierStokes.OutgoingSchedule.shape eta

noncomputable def NavierStokes.OutgoingHistories.initialS (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Initial S, given by 16 * eta ^ 2 - (5 / 12) * d.core.P ^ 2 * shape eta ^ 2.

Equations

• NavierStokes.OutgoingHistories.initialS d eta = 16 * eta ^ 2 - 5 / 12 * d.core.P ^ 2 * NavierStokes.OutgoingSchedule.shape eta ^ 2

noncomputable def NavierStokes.OutgoingHistories.initialPi (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Initial pi, given by SchedulePressure.axisPressure d eta + (5 / 2) * d.core.P ^ 2 * shape eta ^ 2.

Equations

• NavierStokes.OutgoingHistories.initialPi d eta = NavierStokes.SchedulePressure.axisPressure d eta + 5 / 2 * d.core.P ^ 2 * NavierStokes.OutgoingSchedule.shape eta ^ 2

noncomputable def NavierStokes.OutgoingHistories.M (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) : Field

M, given by history initialM (massWeight d Amp).

Equations

• NavierStokes.OutgoingHistories.M d Amp = NavierStokes.OutgoingHistories.history NavierStokes.OutgoingHistories.initialM (NavierStokes.OutgoingHistories.massWeight d Amp)

noncomputable def NavierStokes.OutgoingHistories.I {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : Field

I, given by history (initialI d) (angularWeight w).

Equations

• NavierStokes.OutgoingHistories.I w = NavierStokes.OutgoingHistories.history (NavierStokes.OutgoingHistories.initialI d) (NavierStokes.OutgoingHistories.angularWeight w)

noncomputable def NavierStokes.OutgoingHistories.J {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) : Field

J, given by history (initialJ d) (transportWeight w Amp).

Equations

• NavierStokes.OutgoingHistories.J w Amp = NavierStokes.OutgoingHistories.history (NavierStokes.OutgoingHistories.initialJ d) (NavierStokes.OutgoingHistories.transportWeight w Amp)

noncomputable def NavierStokes.OutgoingHistories.S {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) : Field

S, given by history (initialS d) (energyWeight w Amp).

Equations

• NavierStokes.OutgoingHistories.S w Amp = NavierStokes.OutgoingHistories.history (NavierStokes.OutgoingHistories.initialS d) (NavierStokes.OutgoingHistories.energyWeight w Amp)

noncomputable def NavierStokes.OutgoingHistories.Pi {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : Field

Pi, given by history (initialPi d) (pressureWeight w).

Equations

• NavierStokes.OutgoingHistories.Pi w = NavierStokes.OutgoingHistories.history (NavierStokes.OutgoingHistories.initialPi d) (NavierStokes.OutgoingHistories.pressureWeight w)

theorem NavierStokes.OutgoingHistories.E_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ (↑⊤) (E w)

theorem NavierStokes.OutgoingHistories.E_pos {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : 0 < E w p

theorem NavierStokes.OutgoingHistories.U_smooth (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (U d Amp)

theorem NavierStokes.OutgoingHistories.H_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ (↑⊤) (H w)

theorem NavierStokes.OutgoingHistories.H_pos {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : 0 < H w p

theorem NavierStokes.OutgoingHistories.angularWeight_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : angularWeight w p = Real.exp (3 * p.1 / 2) * E w p

theorem NavierStokes.OutgoingHistories.massWeight_smooth (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (massWeight d Amp)

theorem NavierStokes.OutgoingHistories.angularWeight_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ (↑⊤) (angularWeight w)

theorem NavierStokes.OutgoingHistories.transportWeight_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (transportWeight w Amp)

theorem NavierStokes.OutgoingHistories.energyDensity_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (energyDensity w Amp)

theorem NavierStokes.OutgoingHistories.energyWeight_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (energyWeight w Amp)

theorem NavierStokes.OutgoingHistories.pressureWeight_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ (↑⊤) (pressureWeight w)

theorem NavierStokes.OutgoingHistories.initialM_smooth : ContDiff ℝ (↑⊤) initialM

theorem NavierStokes.OutgoingHistories.initialI_smooth (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (initialI d)

theorem NavierStokes.OutgoingHistories.initialJ_smooth (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (initialJ d)

theorem NavierStokes.OutgoingHistories.initialS_smooth (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (initialS d)

theorem NavierStokes.OutgoingHistories.initialPi_smooth (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (initialPi d)

theorem NavierStokes.OutgoingHistories.M_smooth (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (M d Amp)

theorem NavierStokes.OutgoingHistories.I_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ (↑⊤) (I w)

theorem NavierStokes.OutgoingHistories.J_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (J w Amp)

theorem NavierStokes.OutgoingHistories.S_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (S w Amp)

theorem NavierStokes.OutgoingHistories.Pi_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) : ContDiff ℝ (↑⊤) (Pi w)

theorem NavierStokes.OutgoingHistories.M_hasDerivAt (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => M d Amp (y, p.2)) (X p * U d Amp p) p.1

theorem NavierStokes.OutgoingHistories.I_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : HasDerivAt (fun (y : ℝ) => I w (y, p.2)) (X p * H w p) p.1

theorem NavierStokes.OutgoingHistories.J_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => J w Amp (y, p.2)) (X p * (U d Amp p * H w p)) p.1

theorem NavierStokes.OutgoingHistories.S_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => S w Amp (y, p.2)) (X p * energyDensity w Amp p) p.1

theorem NavierStokes.OutgoingHistories.Pi_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : HasDerivAt (fun (y : ℝ) => Pi w (y, p.2)) (E w p ^ 2 / 2) p.1

theorem NavierStokes.OutgoingHistories.dEta_massWeight (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : dEta (massWeight d Amp) p = X p * dEta (U d Amp) p

theorem NavierStokes.OutgoingHistories.dEta_angularWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : dEta (angularWeight w) p = X p * dEta (H w) p

theorem NavierStokes.OutgoingHistories.dEta_transportWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : dEta (transportWeight w Amp) p = X p * (dEta (U d Amp) p * H w p + U d Amp p * dEta (H w) p)

theorem NavierStokes.OutgoingHistories.dEta_energyDensity {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : dEta (energyDensity w Amp) p = 2 * U d Amp p * dEta (U d Amp) p - E w p * dEta (E w) p

theorem NavierStokes.OutgoingHistories.dEta_energyWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : dEta (energyWeight w Amp) p = X p * (2 * U d Amp p * dEta (U d Amp) p - E w p * dEta (E w) p)

theorem NavierStokes.OutgoingHistories.dEta_pressureWeight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : dEta (pressureWeight w) p = E w p * dEta (E w) p

theorem NavierStokes.OutgoingHistories.dEta_M_hasDerivAt (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => dEta (M d Amp) (y, p.2)) (X p * dEta (U d Amp) p) p.1

theorem NavierStokes.OutgoingHistories.dEta_I_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : HasDerivAt (fun (y : ℝ) => dEta (I w) (y, p.2)) (X p * dEta (H w) p) p.1

theorem NavierStokes.OutgoingHistories.dEta_J_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => dEta (J w Amp) (y, p.2)) (X p * (dEta (U d Amp) p * H w p + U d Amp p * dEta (H w) p)) p.1

theorem NavierStokes.OutgoingHistories.dEta_S_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => dEta (S w Amp) (y, p.2)) (X p * (2 * U d Amp p * dEta (U d Amp) p - E w p * dEta (E w) p)) p.1

theorem NavierStokes.OutgoingHistories.dEta_Pi_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : HasDerivAt (fun (y : ℝ) => dEta (Pi w) (y, p.2)) (E w p * dEta (E w) p) p.1

Transport and the two genuine lags

noncomputable def NavierStokes.OutgoingHistories.XW (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (p : Point) : ℝ

XW, given by X p - 2 * axialExponent d.h * p.2 * M d Amp p - coordinateFactor p.2 * dEta (M d Amp) p.

Equations

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

noncomputable def NavierStokes.OutgoingHistories.W (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (p : Point) : ℝ

W, given by XW d Amp p / X p.

Equations

• NavierStokes.OutgoingHistories.W d Amp p = NavierStokes.OutgoingHistories.XW d Amp p / NavierStokes.OutgoingHistories.X p

noncomputable def NavierStokes.OutgoingHistories.Ubar (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (p : Point) : ℝ

Ubar, given by M d Amp p / X p.

Equations

• NavierStokes.OutgoingHistories.Ubar d Amp p = NavierStokes.OutgoingHistories.M d Amp p / NavierStokes.OutgoingHistories.X p

noncomputable def NavierStokes.OutgoingHistories.angularSource {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Angular source as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingHistories.Sq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Sq, given by angularSource w Amp p / H w p.

Equations

• NavierStokes.OutgoingHistories.Sq w Amp p = NavierStokes.OutgoingHistories.angularSource w Amp p / NavierStokes.OutgoingHistories.H w p

noncomputable def NavierStokes.OutgoingHistories.Sn {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Sn as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingHistories.angularStock {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Angular stock as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingHistories.axialStock {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Axial stock as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingHistories.Qs {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Qs, given by angularStock w Amp p / (X p * H w p).

Equations

• NavierStokes.OutgoingHistories.Qs w Amp p = NavierStokes.OutgoingHistories.angularStock w Amp p / (NavierStokes.OutgoingHistories.X p * NavierStokes.OutgoingHistories.H w p)

noncomputable def NavierStokes.OutgoingHistories.Ns {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Ns, given by axialStock w Amp p / X p.

Equations

• NavierStokes.OutgoingHistories.Ns w Amp p = NavierStokes.OutgoingHistories.axialStock w Amp p / NavierStokes.OutgoingHistories.X p

theorem NavierStokes.OutgoingHistories.XW_smooth (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (XW d Amp)

theorem NavierStokes.OutgoingHistories.W_smooth (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (W d Amp)

theorem NavierStokes.OutgoingHistories.Ubar_smooth (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (Ubar d Amp)

theorem NavierStokes.OutgoingHistories.XW_eq_mul_W (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (p : Point) : XW d Amp p = X p * W d Amp p

theorem NavierStokes.OutgoingHistories.Ubar_parameter (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : dEta (Ubar d Amp) p = dEta (M d Amp) p / X p

theorem NavierStokes.OutgoingHistories.W_formula (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : W d Amp p = 1 - 2 * StressAlgebra.axialExponent d.h * p.2 * Ubar d Amp p - StressAlgebra.coordinateFactor p.2 * dEta (Ubar d Amp) p

theorem NavierStokes.OutgoingHistories.XW_hasDerivAt (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => XW d Amp (y, p.2)) (X p * (1 - 2 * StressAlgebra.axialExponent d.h * p.2 * U d Amp p - StressAlgebra.coordinateFactor p.2 * dEta (U d Amp) p)) p.1

theorem NavierStokes.OutgoingHistories.angularStock_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (angularStock w Amp)

theorem NavierStokes.OutgoingHistories.axialStock_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (axialStock w Amp)

theorem NavierStokes.OutgoingHistories.Qs_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (Qs w Amp)

theorem NavierStokes.OutgoingHistories.Ns_smooth {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : ContDiff ℝ (↑⊤) (Ns w Amp)

theorem NavierStokes.OutgoingHistories.dY_Pi {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : dY (Pi w) p = E w p ^ 2 / 2

theorem NavierStokes.OutgoingHistories.angularStock_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => angularStock w Amp (y, p.2)) (X p * angularSource w Amp p) p.1

theorem NavierStokes.OutgoingHistories.axialStock_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => axialStock w Amp (y, p.2)) (X p * Sn w Amp p) p.1

theorem NavierStokes.OutgoingHistories.Qs_integrated {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : Qs w Amp p = -W d Amp p + ((1 - d.h) * I w p - StressAlgebra.axialExponent d.h * p.2 * dEta (I w) p - StressAlgebra.coordinateFactor p.2 * dEta (J w Amp) p + 2 * (d.h - StressAlgebra.axialExponent d.h) * p.2 * J w Amp p) / (X p * H w p)

Equation (9), with every moment and derivative constructed above.

theorem NavierStokes.OutgoingHistories.Ns_integrated {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : Ns w Amp p = -W d Amp p * U d Amp p + StressAlgebra.axialExponent d.h * (M d Amp p - p.2 * dEta (M d Amp) p) / X p + (4 * d.h * p.2 * S w Amp p - StressAlgebra.coordinateFactor p.2 * dEta (S w Amp) p) / X p + 4 * StressAlgebra.velocityExponent d.h * p.2 * Pi w p - StressAlgebra.coordinateFactor p.2 * dEta (Pi w) p

The axial row of (9) for the same corrected fields as Qs.

theorem NavierStokes.OutgoingHistories.Qs_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => Qs w Amp (y, p.2)) (Sq w Amp p - (1 + dY (H w) p / H w p) * Qs w Amp p) p.1

theorem NavierStokes.OutgoingHistories.Ns_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : HasDerivAt (fun (y : ℝ) => Ns w Amp (y, p.2)) (Sn w Amp p - Ns w Amp p) p.1

theorem NavierStokes.OutgoingHistories.Qs_equation {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : deriv (fun (y : ℝ) => Qs w Amp (y, p.2)) p.1 + (1 + dY (H w) p / H w p) * Qs w Amp p = Sq w Amp p

The angular ODE (6), using the derivative in the true log coordinate.

theorem NavierStokes.OutgoingHistories.Ns_equation {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (p : Point) : deriv (fun (y : ℝ) => Ns w Amp (y, p.2)) p.1 + Ns w Amp p = Sn w Amp p

The axial ODE (6); no derivative identity is an input hypothesis.

theorem NavierStokes.OutgoingHistories.dEta_H {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : Point) : dEta (H w) p = Real.exp (p.1 / 2) * dEta (E w) p

theorem NavierStokes.OutgoingHistories.Sq_formula {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : Sq w Amp p = -W d Amp p * (dY (H w) p / H w p) - d.h * (1 - 2 * p.2 * U d Amp p) - (StressAlgebra.axialExponent d.h * p.2 + StressAlgebra.coordinateFactor p.2 * U d Amp p) * (dEta (E w) p / E w p)

The source as printed in (6), with logarithmic derivatives written as ratios.

The incoming values and the unchanged pre-pulse region

theorem NavierStokes.OutgoingHistories.E_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : E w (y, eta) = OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta)

theorem NavierStokes.OutgoingHistories.E_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : E w (y, eta) = d.core.P * OutgoingSchedule.shape eta * Real.exp (y / 10)

theorem NavierStokes.OutgoingHistories.U_ideal (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : U d Amp (y, eta) = 4 * eta

theorem NavierStokes.OutgoingHistories.U_before_pulse (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.pulseStart) : U d Amp (y, eta) = OutgoingSchedule.dropCoefficient d.core.m y * eta

theorem NavierStokes.OutgoingHistories.M_eq_massMoment (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (y eta : ℝ) : M d Amp (y, eta) = OutgoingSchedule.massMoment d.core Amp eta y

theorem NavierStokes.OutgoingHistories.M_div_E_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : M d Amp (y, eta) / (X (y, eta) * E w (y, eta)) = OutgoingSchedule.massMoment d.core Amp eta y / (Real.exp y * OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta))

@[simp]

theorem NavierStokes.OutgoingHistories.history_zero (initial : ℝ → ℝ) (f : Field) (eta : ℝ) : history initial f (0, eta) = initial eta

theorem NavierStokes.OutgoingHistories.dEta_history_zero {initial : ℝ → ℝ} {f : Field} (hi : ContDiff ℝ (↑⊤) initial) (hf : ContDiff ℝ (↑⊤) f) (eta : ℝ) : dEta (history initial f) (0, eta) = deriv initial eta

@[simp]

theorem NavierStokes.OutgoingHistories.M_zero (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (eta : ℝ) : M d Amp (0, eta) = initialM eta

@[simp]

theorem NavierStokes.OutgoingHistories.I_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : I w (0, eta) = initialI d eta

@[simp]

theorem NavierStokes.OutgoingHistories.J_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) : J w Amp (0, eta) = initialJ d eta

@[simp]

theorem NavierStokes.OutgoingHistories.S_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) : S w Amp (0, eta) = initialS d eta

@[simp]

theorem NavierStokes.OutgoingHistories.Pi_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : Pi w (0, eta) = initialPi d eta

@[simp]

theorem NavierStokes.OutgoingHistories.X_zero (eta : ℝ) : X (0, eta) = 1

@[simp]

theorem NavierStokes.OutgoingHistories.H_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : H w (0, eta) = d.core.P * OutgoingSchedule.shape eta

theorem NavierStokes.OutgoingHistories.dEta_M_zero (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : dEta (M d Amp) (0, eta) = 4

theorem NavierStokes.OutgoingHistories.dEta_I_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : dEta (I w) (0, eta) = 5 / 8 * d.core.P * (OutgoingSchedule.shape eta * -(2 * eta / (1 + eta ^ 2)))

theorem NavierStokes.OutgoingHistories.dEta_J_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : dEta (J w Amp) (0, eta) = 5 / 2 * d.core.P * OutgoingSchedule.shape eta + 5 / 2 * d.core.P * eta * (OutgoingSchedule.shape eta * -(2 * eta / (1 + eta ^ 2)))

theorem NavierStokes.OutgoingHistories.Qs_initial {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : Qs w Amp (0, eta) = (3 / 5 * (4 * (1 - 2 * d.h * eta ^ 2) - 1) - d.h * (1 - 8 * eta ^ 2) + (StressAlgebra.axialExponent d.h + 4 * StressAlgebra.coordinateFactor eta) * eta * (2 * eta / (1 + eta ^ 2))) / (8 / 5)

The incoming angular lag is fixed by the actual ideal-past integrals.

Exact endpoint cancellation for the common fields

theorem NavierStokes.OutgoingHistories.U_after_endpoint (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : U d Amp (y, eta) = 0

theorem NavierStokes.OutgoingHistories.angular_product_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (y eta : ℝ) : E w (y, eta) * U d Amp (y, eta) = OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta) * U d Amp (y, eta)

theorem NavierStokes.OutgoingHistories.transportWeight_eq_core {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (y eta : ℝ) : transportWeight w Amp (y, eta) = Real.exp (3 * y / 2) * OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta) * U d Amp (y, eta)

theorem NavierStokes.OutgoingHistories.J_eq_angularMoment {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (y eta : ℝ) : √2 * J w Amp (y, eta) = OutgoingSchedule.angularMoment d.core Amp eta y

theorem NavierStokes.OutgoingHistories.M_after_endpoint (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : M d Amp (y, eta) = 0

theorem NavierStokes.OutgoingHistories.J_after_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : J w Amp (y, eta) = 0

theorem NavierStokes.OutgoingHistories.dEta_M_after_endpoint (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : dEta (M d Amp) (y, eta) = 0

theorem NavierStokes.OutgoingHistories.dEta_J_after_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : dEta (J w Amp) (y, eta) = 0

theorem NavierStokes.OutgoingHistories.W_after_endpoint (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : W d Amp (y, eta) = 1

theorem NavierStokes.OutgoingHistories.Qs_after_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : Qs w Amp (y, eta) = -1 + ((1 - d.h) * I w (y, eta) - StressAlgebra.axialExponent d.h * eta * dEta (I w) (y, eta)) / (Real.exp (3 * y / 2) * E w (y, eta))

theorem NavierStokes.OutgoingHistories.Ns_after_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.endpoint ≤ y) : Ns w Amp (y, eta) = (4 * d.h * eta * S w Amp (y, eta) - StressAlgebra.coordinateFactor eta * dEta (S w Amp) (y, eta)) / Real.exp y + 4 * StressAlgebra.velocityExponent d.h * eta * Pi w (y, eta) - StressAlgebra.coordinateFactor eta * dEta (Pi w) (y, eta)

Identification with actual improper past integrals

theorem NavierStokes.OutgoingHistories.past_integrable {f : ℝ → ℝ} (hf : Continuous f) (h0 : MeasureTheory.IntegrableOn f (Set.Iic 0) MeasureTheory.volume) (y : ℝ) : MeasureTheory.IntegrableOn f (Set.Iic y) MeasureTheory.volume

theorem NavierStokes.OutgoingHistories.past_integral {f : ℝ → ℝ} (hf : Continuous f) (h0 : MeasureTheory.IntegrableOn f (Set.Iic 0) MeasureTheory.volume) (y : ℝ) : ∫ (t : ℝ) in Set.Iic y, f t = (∫ (t : ℝ) in Set.Iic 0, f t) + ∫ (t : ℝ) in 0..y, f t

theorem NavierStokes.OutgoingHistories.exponential_past {f : ℝ → ℝ} (a b : ℝ) (hb : 0 < b) (he : ∀ y ≤ 0, f y = a * Real.exp (b * y)) : MeasureTheory.IntegrableOn f (Set.Iic 0) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Iic 0, f t = a / b

theorem NavierStokes.OutgoingHistories.mass_past (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => massWeight d Amp (y, eta)) (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, massWeight d Amp (y, eta) = initialM eta

theorem NavierStokes.OutgoingHistories.angularWeight_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : angularWeight w (y, eta) = d.core.P * OutgoingSchedule.shape eta * Real.exp (8 / 5 * y)

theorem NavierStokes.OutgoingHistories.angular_past {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => angularWeight w (y, eta)) (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, angularWeight w (y, eta) = initialI d eta

theorem NavierStokes.OutgoingHistories.transport_past {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => transportWeight w Amp (y, eta)) (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, transportWeight w Amp (y, eta) = initialJ d eta

theorem NavierStokes.OutgoingHistories.weighted_square_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (b eta : ℝ) {y : ℝ} (hy : y ≤ 0) : Real.exp (b * y) * E w (y, eta) ^ 2 / 2 = d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 / 2 * Real.exp ((b + 1 / 5) * y)

theorem NavierStokes.OutgoingHistories.energy_past {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => energyWeight w Amp (y, eta)) (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, energyWeight w Amp (y, eta) = initialS d eta

theorem NavierStokes.OutgoingHistories.pressure_past {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => pressureWeight w (y, eta)) (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, pressureWeight w (y, eta) = 5 / 2 * d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2

theorem NavierStokes.OutgoingHistories.M_eq_integral (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : M d Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, Real.exp t * U d Amp (t, eta)

theorem NavierStokes.OutgoingHistories.I_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : I w (y, eta) = ∫ (t : ℝ) in Set.Iic y, Real.exp (3 * t / 2) * E w (t, eta)

theorem NavierStokes.OutgoingHistories.J_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : J w Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, Real.exp (3 * t / 2) * E w (t, eta) * U d Amp (t, eta)

theorem NavierStokes.OutgoingHistories.S_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : S w Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, Real.exp t * (U d Amp (t, eta) ^ 2 - E w (t, eta) ^ 2 / 2)

theorem NavierStokes.OutgoingHistories.Pi_eq_past_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : Pi w (y, eta) = SchedulePressure.axisPressure d eta + ∫ (t : ℝ) in Set.Iic y, E w (t, eta) ^ 2 / 2

The same corrected field fixes the canonical pressure

theorem NavierStokes.OutgoingHistories.E_square_integrable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => E w (y, eta) ^ 2) MeasureTheory.volume

theorem NavierStokes.OutgoingHistories.E_square_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) : ∫ (y : ℝ), E w (y, eta) ^ 2 = ∫ (y : ℝ), OutgoingTail.finalAngular d (y, eta) ^ 2

theorem NavierStokes.OutgoingHistories.Pi_eq_future_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : Pi w (y, eta) = -(1 / 2) * ∫ (t : ℝ) in Set.Ioi y, E w (t, eta) ^ 2

theorem NavierStokes.OutgoingHistories.energyWeight_integrable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => energyWeight w Amp (y, eta)) MeasureTheory.volume

theorem NavierStokes.OutgoingHistories.total_energy_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (eta : ℝ) : ∫ (y : ℝ), energyWeight w Amp (y, eta) = CorrectedPulseAmplitude.totalEnergy d w.coefficients (Amp eta) eta

theorem NavierStokes.OutgoingHistories.angular_source_continuous {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : Continuous fun (y : ℝ) => X (y, eta) * angularSource w Amp (y, eta)

theorem NavierStokes.OutgoingHistories.axial_source_continuous {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : Continuous fun (y : ℝ) => X (y, eta) * Sn w Amp (y, eta)

theorem NavierStokes.OutgoingHistories.angularStock_eq_source_primitive {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : angularStock w Amp (y, eta) = angularStock w Amp (0, eta) + ∫ (t : ℝ) in 0..y, X (t, eta) * angularSource w Amp (t, eta)

theorem NavierStokes.OutgoingHistories.axialStock_eq_source_primitive {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : axialStock w Amp (y, eta) = axialStock w Amp (0, eta) + ∫ (t : ℝ) in 0..y, X (t, eta) * Sn w Amp (t, eta)

theorem NavierStokes.OutgoingHistories.exponential_integral_left {f : ℝ → ℝ} (a b : ℝ) (hb : 0 < b) (he : ∀ t ≤ 0, f t = a * Real.exp (b * t)) {y : ℝ} (hy : y ≤ 0) : ∫ (t : ℝ) in Set.Iic y, f t = a / b * Real.exp (b * y)

theorem NavierStokes.OutgoingHistories.derivative_from_left {f g : ℝ → ℝ} {v y : ℝ} (hy : y ≤ 0) (hf : DifferentiableAt ℝ f y) (hg : HasDerivAt g v y) (he : ∀ t ≤ 0, f t = g t) : HasDerivAt f v y

A left closed interval determines the derivative even at its endpoint.

theorem NavierStokes.OutgoingHistories.M_ideal (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : M d Amp (y, eta) = 4 * eta * Real.exp y

theorem NavierStokes.OutgoingHistories.dEta_M_ideal (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : dEta (M d Amp) (y, eta) = 4 * Real.exp y

theorem NavierStokes.OutgoingHistories.W_ideal (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : W d Amp (y, eta) = 1 - 4 * (1 - 2 * d.h * eta ^ 2)

theorem NavierStokes.OutgoingHistories.Pi_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : Pi w (y, eta) = SchedulePressure.axisPressure d eta + 5 / 2 * d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * Real.exp (y / 5)

noncomputable def NavierStokes.OutgoingHistories.shapeRate (eta : ℝ) : ℝ

Shape rate, given by 2 * eta / (1 + eta ^ 2).

Equations

• NavierStokes.OutgoingHistories.shapeRate eta = 2 * eta / (1 + eta ^ 2)

theorem NavierStokes.OutgoingHistories.dEta_E_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : dEta (E w) (y, eta) = -(E w (y, eta) * shapeRate eta)

theorem NavierStokes.OutgoingHistories.dY_H_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : dY (H w) (y, eta) = 3 / 5 * H w (y, eta)

theorem NavierStokes.OutgoingHistories.dY_U_ideal (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : dY (U d Amp) (y, eta) = 0

theorem NavierStokes.OutgoingHistories.dEta_U_ideal (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : dEta (U d Amp) (y, eta) = 4

theorem NavierStokes.OutgoingHistories.dEta_Pi_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : dEta (Pi w) (y, eta) = deriv (SchedulePressure.axisPressure d) eta - 5 * d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * shapeRate eta * Real.exp (y / 5)

The ideal past also fixes the source primitives

noncomputable def NavierStokes.OutgoingHistories.incomingSq (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Incoming sq as an element of ℝ.

Equations

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

theorem NavierStokes.OutgoingHistories.Sq_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : Sq w Amp (y, eta) = incomingSq d eta

theorem NavierStokes.OutgoingHistories.angularSource_weight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : X p * angularSource w Amp p = angularWeight w p * Sq w Amp p

theorem NavierStokes.OutgoingHistories.angular_source_past {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => X (y, eta) * angularSource w Amp (y, eta)) (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, X (y, eta) * angularSource w Amp (y, eta) = angularStock w Amp (0, eta)

theorem NavierStokes.OutgoingHistories.angularStock_eq_source_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : angularStock w Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, X (t, eta) * angularSource w Amp (t, eta)

theorem NavierStokes.OutgoingHistories.Qs_eq_source_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : Qs w Amp (y, eta) = (∫ (t : ℝ) in Set.Iic y, Real.exp (3 * t / 2) * E w (t, eta) * Sq w Amp (t, eta)) / (Real.exp (3 * y / 2) * E w (y, eta))

The regular source-integral definition of Q_s, including its actual past.

noncomputable def NavierStokes.OutgoingHistories.incomingSnConstant (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Incoming sn constant as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingHistories.incomingSnGrowing (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Incoming sn growing, given by d.core.P ^ 2 * shape eta ^ 2 * (5 * coordinateFactor eta * shapeRate eta + (10 * velocityExponent d.h + 1) * eta).

Equations

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

theorem NavierStokes.OutgoingHistories.Sn_ideal {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : y ≤ 0) : Sn w Amp (y, eta) = incomingSnConstant d eta + incomingSnGrowing d eta * Real.exp (y / 5)

theorem NavierStokes.OutgoingHistories.dEta_S_zero {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : dEta (S w Amp) (0, eta) = 32 * eta + 5 / 6 * d.core.P ^ 2 * OutgoingSchedule.shape eta ^ 2 * shapeRate eta

theorem NavierStokes.OutgoingHistories.axialStock_initial {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : axialStock w Amp (0, eta) = incomingSnConstant d eta + 5 / 6 * incomingSnGrowing d eta

theorem NavierStokes.OutgoingHistories.exponential_sum_past {f : ℝ → ℝ} (a b c e : ℝ) (hb : 0 < b) (he : 0 < e) (hf : ∀ y ≤ 0, f y = a * Real.exp (b * y) + c * Real.exp (e * y)) : MeasureTheory.IntegrableOn f (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, f y = a / b + c / e

theorem NavierStokes.OutgoingHistories.axial_source_past {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) : MeasureTheory.IntegrableOn (fun (y : ℝ) => X (y, eta) * Sn w Amp (y, eta)) (Set.Iic 0) MeasureTheory.volume ∧ ∫ (y : ℝ) in Set.Iic 0, X (y, eta) * Sn w Amp (y, eta) = axialStock w Amp (0, eta)

theorem NavierStokes.OutgoingHistories.axialStock_eq_source_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : axialStock w Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, X (t, eta) * Sn w Amp (t, eta)

theorem NavierStokes.OutgoingHistories.Ns_eq_source_integral {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : Ns w Amp (y, eta) = (∫ (t : ℝ) in Set.Iic y, Real.exp t * Sn w Amp (t, eta)) / Real.exp y

The regular source-integral definition of N_s, including its actual past.

Entrance-radius factors

noncomputable def NavierStokes.OutgoingHistories.physicalX (XR : ℝ) (p : Point) : ℝ

Physical X, given by XR * X p.

Equations

• NavierStokes.OutgoingHistories.physicalX XR p = XR * NavierStokes.OutgoingHistories.X p

noncomputable def NavierStokes.OutgoingHistories.physicalH {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (p : Point) : ℝ

Physical H, given by Real.sqrt (2 * XR) * H w p.

Equations

• NavierStokes.OutgoingHistories.physicalH XR w p = √(2 * XR) * NavierStokes.OutgoingHistories.H w p

noncomputable def NavierStokes.OutgoingHistories.physicalM (XR : ℝ) (d : OutgoingTail.TailData) (Amp : ℝ → ℝ) (p : Point) : ℝ

Physical M, given by XR * M d Amp p.

Equations

• NavierStokes.OutgoingHistories.physicalM XR d Amp p = XR * NavierStokes.OutgoingHistories.M d Amp p

noncomputable def NavierStokes.OutgoingHistories.physicalI {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (p : Point) : ℝ

Physical I, given by XR * Real.sqrt (2 * XR) * I w p.

Equations

• NavierStokes.OutgoingHistories.physicalI XR w p = XR * √(2 * XR) * NavierStokes.OutgoingHistories.I w p

noncomputable def NavierStokes.OutgoingHistories.physicalJ {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Physical J, given by XR * Real.sqrt (2 * XR) * J w Amp p.

Equations

• NavierStokes.OutgoingHistories.physicalJ XR w Amp p = XR * √(2 * XR) * NavierStokes.OutgoingHistories.J w Amp p

noncomputable def NavierStokes.OutgoingHistories.physicalS {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

Physical S, given by XR * S w Amp p.

Equations

• NavierStokes.OutgoingHistories.physicalS XR w Amp p = XR * NavierStokes.OutgoingHistories.S w Amp p

theorem NavierStokes.OutgoingHistories.physicalH_eq {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (hXR : 0 < XR) (w : UniformAngularReset.ResetWitness d K) (p : Point) : physicalH XR w p = √(2 * physicalX XR p) * E w p

theorem NavierStokes.OutgoingHistories.physicalM_eq_integral (XR : ℝ) (d : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : physicalM XR d Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, physicalX XR (t, eta) * U d Amp (t, eta)

theorem NavierStokes.OutgoingHistories.physicalI_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : physicalI XR w (y, eta) = ∫ (t : ℝ) in Set.Iic y, physicalX XR (t, eta) * physicalH XR w (t, eta)

theorem NavierStokes.OutgoingHistories.physicalJ_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : physicalJ XR w Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, physicalX XR (t, eta) * (U d Amp (t, eta) * physicalH XR w (t, eta))

theorem NavierStokes.OutgoingHistories.physicalS_eq_integral {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : physicalS XR w Amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, physicalX XR (t, eta) * (U d Amp (t, eta) ^ 2 - E w (t, eta) ^ 2 / 2)

theorem NavierStokes.OutgoingHistories.Qs_dilation {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (hXR : 0 < XR) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : XR * √(2 * XR) * angularStock w Amp p / (physicalX XR p * physicalH XR w p) = Qs w Amp p

The common angular scaling cancels exactly from the source-integral lag.

theorem NavierStokes.OutgoingHistories.Ns_dilation {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (hXR : 0 < XR) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : XR * axialStock w Amp p / physicalX XR p = Ns w Amp p

The common axial scaling cancels exactly from the source-integral lag.

noncomputable def NavierStokes.OutgoingHistories.p1 {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

P1, given by physicalX XR p * Qs w Amp p / (1 - 2 * d.h * p.2 ^ 2).

Equations

• NavierStokes.OutgoingHistories.p1 XR w Amp p = NavierStokes.OutgoingHistories.physicalX XR p * NavierStokes.OutgoingHistories.Qs w Amp p / (1 - 2 * d.h * p.2 ^ 2)

noncomputable def NavierStokes.OutgoingHistories.p2 {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : ℝ

P2, given by physicalX XR p * Ns w Amp p / ((1 - 2 * d.h * p.2 ^ 2) * E w p).

Equations

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

theorem NavierStokes.OutgoingHistories.p1_dilation {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : p1 XR w Amp p = XR * p1 1 w Amp p

theorem NavierStokes.OutgoingHistories.p2_dilation {d : OutgoingTail.TailData} {K : ℝ} (XR : ℝ) (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : Point) : p2 XR w Amp p = XR * p2 1 w Amp p