The pressure datum of the constructed outgoing angular schedule

This module instantiates the abstract pressure integral with finalAngular. The pressure-neutral angular-moment correction remains a separate operation.

noncomputable def NavierStokes.SchedulePressure.clockWeight (d : OutgoingTail.TailData) (y : ℝ) : ℝ

Squared clock amplitude, taken from the actual angular schedule at η=0.

Equations

• NavierStokes.SchedulePressure.clockWeight d y = NavierStokes.OutgoingTail.finalAngular d (y, 0) ^ 2

noncomputable def NavierStokes.SchedulePressure.shapeExponent (d : OutgoingTail.TailData) (y : ℝ) : ℝ

The shape exponent decreases from one to zero during flattening.

Equations

• NavierStokes.SchedulePressure.shapeExponent d y = 1 - NavierStokes.OutgoingSchedule.sigma ((y - d.core.endpoint) / NavierStokes.OutgoingTail.flattenLength)

noncomputable def NavierStokes.SchedulePressure.axisPressure (d : OutgoingTail.TailData) (η : ℝ) : ℝ

The datum computed directly from the complete constructed angular field.

Equations

• NavierStokes.SchedulePressure.axisPressure d η = -(1 / 2) * ∫ (y : ℝ), NavierStokes.OutgoingTail.finalAngular d (y, η) ^ 2

theorem NavierStokes.SchedulePressure.endpoint_pos (d : OutgoingTail.TailData) : 0 < d.core.endpoint

theorem NavierStokes.SchedulePressure.clockWeight_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (clockWeight d)

theorem NavierStokes.SchedulePressure.clockWeight_pos (d : OutgoingTail.TailData) (y : ℝ) : 0 < clockWeight d y

theorem NavierStokes.SchedulePressure.shapeExponent_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (shapeExponent d)

theorem NavierStokes.SchedulePressure.shapeExponent_bounds (d : OutgoingTail.TailData) (y : ℝ) : 0 ≤ shapeExponent d y ∧ shapeExponent d y ≤ 1

theorem NavierStokes.SchedulePressure.shapeExponent_before (d : OutgoingTail.TailData) {y : ℝ} (hy : y ≤ d.core.endpoint) : shapeExponent d y = 1

theorem NavierStokes.SchedulePressure.shapeExponent_after (d : OutgoingTail.TailData) {y : ℝ} (hy : d.flattenEnd ≤ y) : shapeExponent d y = 0

theorem NavierStokes.SchedulePressure.clockWeight_ideal (d : OutgoingTail.TailData) {y : ℝ} (hy : y ≤ 0) : clockWeight d y = d.core.P ^ 2 * Real.exp (1 / 5 * y)

theorem NavierStokes.SchedulePressure.shape_eq_exp (η : ℝ) : OutgoingSchedule.shape η = Real.exp (-Real.log (1 + η ^ 2))

theorem NavierStokes.SchedulePressure.angular_factorization (d : OutgoingTail.TailData) (y η : ℝ) : OutgoingTail.finalAngular d (y, η) = OutgoingTail.finalAngular d (y, 0) * Real.exp (-shapeExponent d y * Real.log (1 + η ^ 2))

Exact shape separation of the complete angular schedule.

theorem NavierStokes.SchedulePressure.angular_square_factorization (d : OutgoingTail.TailData) (y η : ℝ) : OutgoingTail.finalAngular d (y, η) ^ 2 = clockWeight d y * PressureDatum.kernel (shapeExponent d y) η

theorem NavierStokes.SchedulePressure.clockWeight_integrable_left (d : OutgoingTail.TailData) : MeasureTheory.IntegrableOn (clockWeight d) (Set.Iic 0) MeasureTheory.volume

theorem NavierStokes.SchedulePressure.clockWeight_integrable_right (d : OutgoingTail.TailData) : MeasureTheory.IntegrableOn (clockWeight d) (Set.Ioi d.core.endpoint) MeasureTheory.volume

theorem NavierStokes.SchedulePressure.clockWeight_integrable (d : OutgoingTail.TailData) : MeasureTheory.Integrable (clockWeight d) MeasureTheory.volume

theorem NavierStokes.SchedulePressure.admissible (d : OutgoingTail.TailData) : PressureDatum.Admissible (clockWeight d) (shapeExponent d) 1

The actual schedule discharges all abstract weight/exponent hypotheses.

theorem NavierStokes.SchedulePressure.axisPressure_eq (d : OutgoingTail.TailData) : axisPressure d = PressureDatum.pressure (clockWeight d) (shapeExponent d)

theorem NavierStokes.SchedulePressure.shapeExponent_ideal (d : OutgoingTail.TailData) {y : ℝ} (hy : y ≤ 0) : shapeExponent d y = 1

theorem NavierStokes.SchedulePressure.angular_square_integrable (d : OutgoingTail.TailData) (η : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => OutgoingTail.finalAngular d (y, η) ^ 2) MeasureTheory.volume

theorem NavierStokes.SchedulePressure.axisPressure_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (axisPressure d)

@[simp]

theorem NavierStokes.SchedulePressure.axisPressure_even (d : OutgoingTail.TailData) (η : ℝ) : axisPressure d (-η) = axisPressure d η

theorem NavierStokes.SchedulePressure.axisPressure_lower_bound (d : OutgoingTail.TailData) (η : ℝ) : axisPressure d η ≤ -(5 / 2) * d.core.P ^ 2 * OutgoingSchedule.shape η ^ 2

theorem NavierStokes.SchedulePressure.positive_exponent_mass (d : OutgoingTail.TailData) : 0 < ∫ (y : ℝ), clockWeight d y * shapeExponent d y

theorem NavierStokes.SchedulePressure.axisPressure_hasDerivAt (d : OutgoingTail.TailData) (η : ℝ) : HasDerivAt (axisPressure d) (2 * η / (1 + η ^ 2) * ∫ (y : ℝ), shapeExponent d y * OutgoingTail.finalAngular d (y, η) ^ 2) η

theorem NavierStokes.SchedulePressure.axisPressure_deriv_pos (d : OutgoingTail.TailData) {η : ℝ} (hη : 0 < η) : 0 < deriv (axisPressure d) η

theorem NavierStokes.SchedulePressure.axisPressure_deriv_neg (d : OutgoingTail.TailData) {η : ℝ} (hη : η < 0) : deriv (axisPressure d) η < 0

@[simp]

theorem NavierStokes.SchedulePressure.axisPressure_deriv_zero (d : OutgoingTail.TailData) : deriv (axisPressure d) 0 = 0

theorem NavierStokes.SchedulePressure.axisPressure_neg (d : OutgoingTail.TailData) (η : ℝ) : axisPressure d η < 0

theorem NavierStokes.SchedulePressure.axisPressure_radius_independent (d : OutgoingTail.TailData) (X_R η : ℝ) : -(1 / 2) * ∫ (y : ℝ), OutgoingTail.finalAngular d (y - Real.log X_R, η) ^ 2 = axisPressure d η

Moving X_R translates the logarithmic clock and leaves the actual datum fixed.

noncomputable def NavierStokes.SchedulePressure.complexAxisPressure (d : OutgoingTail.TailData) : ℂ → ℂ

Complex axis pressure, given by PressureDatum.complexPressure (clockWeight d) (shapeExponent d).

Equations

• NavierStokes.SchedulePressure.complexAxisPressure d = NavierStokes.PressureDatum.complexPressure (NavierStokes.SchedulePressure.clockWeight d) (NavierStokes.SchedulePressure.shapeExponent d)

theorem NavierStokes.SchedulePressure.complexAxisPressure_analytic (d : OutgoingTail.TailData) : AnalyticOnNhd ℂ (complexAxisPressure d) PressureDatum.strip

@[simp]

theorem NavierStokes.SchedulePressure.complexAxisPressure_ofReal (d : OutgoingTail.TailData) (η : ℝ) : complexAxisPressure d ↑η = ↑(axisPressure d η)

theorem NavierStokes.SchedulePressure.natural_axis_pressureData (d : OutgoingTail.TailData) (hP : 2 ≤ d.core.P) : NaturalAxisData.PressureData (axisPressure d)

theorem NavierStokes.SchedulePressure.natural_profileFamily (d : OutgoingTail.TailData) {j : ℝ} (hsmall : NaturalAxisData.SmallParameters d.h j) (hP : 2 ≤ d.core.P) : ∃ (δ : ℝ) (σ : ℝ), 0 < δ ∧ 0 < σ ∧ (∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z d.h j (axisPressure d) η| ≤ δ → 99 / 100 < NaturalAxisData.chi d.h j σ η) ∧ ∃ (data : NaturalAxisCoefficients.AnalyticInputs d.h j σ (axisPressure d)) (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (C : ℝ), data.normalizationThreshold Λ ≤ C → Nonempty (NaturalProfile.ProfileFamily data Λ C)

The analytic input is fixed first, followed by every sufficiently large Λ and every normalization C above its constructed threshold.

theorem NavierStokes.SchedulePressure.exists_natural_profiles (d : OutgoingTail.TailData) {j : ℝ} (hsmall : NaturalAxisData.SmallParameters d.h j) (hP : 2 ≤ d.core.P) : ∃ (δ : ℝ) (σ : ℝ) (Λ : ℝ) (C : ℝ), 0 < δ ∧ 0 < σ ∧ 0 < Λ ∧ 0 < C ∧ ∃ (f : ℝ × ℝ → ℝ) (U : ℝ × ℝ → ℝ) (V : ℝ × ℝ → ℝ) (Pr : ℝ × ℝ → ℝ), NaturalProfile.IsNaturalSolution d.h j Λ (axisPressure d) (NaturalAxisCoefficients.realAmplitude d.h j σ Λ C) f U V Pr ∧ (∀ p ∈ NaturalProfile.domain Λ, 0 ≤ Λ * p.1 → Λ * p.1 ≤ 41 / 10 → 0 < f p) ∧ ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z d.h j (axisPressure d) η| ≤ δ → 23 / 10 < -2 * (4 / Λ) * NaturalAxisBridge.partialY f (4 / Λ, η) / f (4 / Λ, η)

The pressure of the actual outgoing schedule supplies the natural-axis theorem.