The next literal activation and horizon are constructed from the current actual frame. Restriction preserves the actual Euler state, low bounds and frame before the next packet is added.

Restricting the actual parent frame to the next packet horizon, and identifying its physical and scaled times with the literal scales.

def EulerPacketSourceGeometry.ParentFrame.restrictTime {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : ParentFrame ((A.restrictTime S hS hST).transverseData m hm R support hSupport) τ

Restrict time, bundling B, B₁, m, v and the required compatibility proofs.

Equations

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

@[simp]

theorem EulerPacketSourceGeometry.ParentFrame.restrictTime_a {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : (P.restrictTime S hS hST hτ).a = P.a

@[simp]

theorem EulerPacketSourceGeometry.ParentFrame.restrictTime_sigma {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : (P.restrictTime S hS hST hτ).sigma = P.sigma

@[simp]

theorem EulerPacketSourceGeometry.ParentFrame.restrictTime_shear {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : (P.restrictTime S hS hST hτ).shear = P.shear

@[simp]

theorem EulerPacketSourceGeometry.ParentFrame.restrictTime_epsilon {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : (P.restrictTime S hS hST hτ).epsilon = P.epsilon

@[simp]

theorem EulerPacketSourceGeometry.ParentFrame.restrictTime_G {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : (P.restrictTime S hS hST hτ).G = P.G

@[simp]

theorem EulerPacketSourceGeometry.ParentFrame.restrictTime_error {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : (P.restrictTime S hS hST hτ).error = P.error

@[simp]

theorem EulerPacketSourceGeometry.ParentFrame.restrictTime_horizon {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) : (P.restrictTime S hS hST hτ).horizon = P.a * (S - τ) / P.epsilon

theorem EulerParentStageHorizon.scaled_rate {a h : ℝ} (ha : 0 ≤ a) : a / √(a / h) = √(a * h)

theorem EulerParentStageHorizon.physical_rate {a h : ℝ} (ha : 0 ≤ a) : √(a / h) / a = 1 / √(a * h)

theorem EulerParentStageHorizon.physical_target_identity {a h β : ℝ} (ha : 0 ≤ a) (hβ : 0 ≤ β) (τ x : ℝ) : EulerPacketMovingFrame.physicalTime τ a (√(a / h)) (x / √β) = τ + x / √(β * a * h)

theorem EulerParentStageHorizon.scaled_horizon_identity {a h β : ℝ} (ha : 0 < a) (hh : 0 < h) (hβ : 0 < β) (τ x W : ℝ) : a * (τ + x / √(β * a * h) + 2 * W - τ) / √(a / h) = x / √β + 2 * √(a * h) * W

theorem EulerPacketSourceGeometry.ParentFrame.target_on_scales {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (J : ℕ) (X : ℝ) (a β : ℕ → ℝ) (n : ℕ) (ha : 0 ≤ a n) (hβ : 0 ≤ β n) (haMatch : P.a = a n) (hShear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n) (hSigma : P.sigma = √(β n)) : EulerPacketMovingFrame.physicalTime τ P.a P.epsilon (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1) / P.sigma) = τ + EulerPacketNestedHorizons.stepLength J X a β n

theorem EulerPacketSourceGeometry.ParentFrame.restricted_horizon_on_scales {A : EulerParentPacketFrames.Parent} {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {m : EulerSmoothLimit.Space} {hm : ‖m‖ = 1} {R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)} {support : Set EulerSmoothLimit.Space} {hSupport : IsCompact support} {τ : ℝ} (P : ParentFrame (A.transverseData m hm R support hSupport) τ) (J : ℕ) (X : ℝ) (hX : 0 < X) (a β : ℕ → ℝ) (n : ℕ) (ha : 0 < a n) (hβ : 0 < β n) (haMatch : P.a = a n) (hShear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) (hτ : 0 ≤ τ) (hSMatch : S = τ + EulerPacketNestedHorizons.stepLength J X a β n + 2 * EulerPacketSourceScaleSequence.timeWidth J X (n + 1)) : (P.restrictTime S hS hST hτ).horizon = EulerPacketSourceScaleGuards.horizon J X (a n) (β n) n

noncomputable def EulerPacketInduction.Stage.step {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : ℝ

Step, given by stepLength S.J S.X (fun _ => P.frame.a) (fun _ => P.frame.sigma^2) n.

Equations

• P.step = EulerPacketNestedHorizons.stepLength S.J S.X (fun (x : ℕ) => P.frame.a) (fun (x : ℕ) => P.frame.sigma ^ 2) n

noncomputable def EulerPacketInduction.Stage.nextTime {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : ℝ

Next time, given by P.time+P.step.

Equations

• P.nextTime = P.time + P.step

noncomputable def EulerPacketInduction.Stage.nextHorizon {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : ℝ

Next horizon, given by P.nextTime+2*timeWidth S.J S.X (n+1).

Equations

• P.nextHorizon = P.nextTime + 2 * EulerPacketSourceScaleSequence.timeWidth S.J S.X (n + 1)

theorem EulerPacketInduction.Stage.step_bounds {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerPacketSourceScaleSequence.timeWidth S.J S.X n / 6 ≤ P.step ∧ P.step ≤ 2 * EulerPacketSourceScaleSequence.timeWidth S.J S.X n / 3

theorem EulerPacketInduction.Stage.step_pos {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : 0 < P.step

theorem EulerPacketInduction.Stage.time_lt_nextTime {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.time < P.nextTime

theorem EulerPacketInduction.Stage.nextTime_pos {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : 0 < P.nextTime

theorem EulerPacketInduction.Stage.nextTime_lt_nextHorizon {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.nextTime < P.nextHorizon

theorem EulerPacketInduction.Stage.time_lt_nextHorizon {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.time < P.nextHorizon

theorem EulerPacketInduction.Stage.nextHorizon_pos {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : 0 < P.nextHorizon

theorem EulerPacketInduction.Stage.nextHorizon_lt {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.nextHorizon < P.parent.T

theorem EulerPacketInduction.Stage.nextHorizon_le {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.nextHorizon ≤ P.parent.T

theorem EulerPacketInduction.Stage.nextHorizon_le_base {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.nextHorizon ≤ EulerPacketBaseGuardScales.baseHorizon S.J S.X

theorem EulerPacketInduction.Stage.nextHorizon_one {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.nextHorizon ≤ 1

theorem EulerPacketInduction.Stage.nextTime_lower {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerPacketBaseGuardScales.baseHorizon S.J S.X / 12 ≤ P.nextTime

theorem EulerPacketInduction.Stage.nextHorizon_common {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerPacketBaseGuardScales.baseHorizon S.J S.X / 12 < P.nextHorizon

theorem EulerPacketInduction.Stage.physical_target_eq_nextTime {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerPacketMovingFrame.physicalTime P.time P.frame.a P.frame.epsilon (EulerPacketSourceScaleChoice.scaleSequence S.J S.X (n + 1) / P.frame.sigma) = P.nextTime

noncomputable def EulerPacketInduction.Stage.restrictedParent {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerParentPacketFrames.Parent

Restricted parent, given by P.parent.restrictTime P.nextHorizon P.nextHorizon_pos P.nextHorizon_le.

Equations

• P.restrictedParent = P.parent.restrictTime P.nextHorizon ⋯ ⋯

noncomputable def EulerPacketInduction.Stage.restrictedState {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerParentPacketFrames.SmoothState P.restrictedParent

Restricted state, given by P.state.restrictTime P.nextHorizon P.nextHorizon_pos P.nextHorizon_le.

Equations

• P.restrictedState = P.state.restrictTime P.nextHorizon ⋯ ⋯

noncomputable def EulerPacketInduction.Stage.restrictedLow {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerParentPacketFrames.LowBounds P.restrictedParent

Restricted low, given by P.low.restrictTime P.nextHorizon P.nextHorizon_pos P.nextHorizon_le.

Equations

• P.restrictedLow = P.low.restrictTime P.nextHorizon ⋯ ⋯

noncomputable def EulerPacketInduction.Stage.restrictedFrame {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : EulerPacketSourceGeometry.ParentFrame (frameData P.restrictedParent) P.time

Restricted frame, given by P.frame.restrictTime P.nextHorizon P.nextHorizon_pos P.nextHorizon_le P.time_nonneg.

Equations

• P.restrictedFrame = P.frame.restrictTime P.nextHorizon ⋯ ⋯ ⋯

@[simp]

theorem EulerPacketInduction.Stage.restrictedParent_time {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedParent.T = P.nextHorizon

@[simp]

theorem EulerPacketInduction.Stage.restrictedParent_scale {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedParent.ell = P.parent.ell

@[simp]

theorem EulerPacketInduction.Stage.restrictedState_label {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedState.labels.K = P.state.labels.K

@[simp]

theorem EulerPacketInduction.Stage.restrictedLow_exterior {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedLow.Be = P.low.Be

@[simp]

theorem EulerPacketInduction.Stage.restrictedLow_core {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedLow.Bc = P.low.Bc

@[simp]

theorem EulerPacketInduction.Stage.restrictedLow_pressure {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedLow.K = P.low.K

@[simp]

theorem EulerPacketInduction.Stage.restrictedLow_boundary {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedLow.L = P.low.L

@[simp]

theorem EulerPacketInduction.Stage.restrictedLow_radius {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedLow.r = P.low.r

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_a {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.a = P.frame.a

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_sigma {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.sigma = P.frame.sigma

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_shear {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.shear = P.frame.shear

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_G {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.G = P.frame.G

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_error {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.error = P.frame.error

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_B {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.B = P.frame.B

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_m {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.m = P.frame.m

@[simp]

theorem EulerPacketInduction.Stage.restrictedFrame_v {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.v = P.frame.v

theorem EulerPacketInduction.Stage.restrictedFrame_horizon {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedFrame.horizon = EulerPacketSourceScaleGuards.horizon S.J S.X P.frame.a (P.frame.sigma ^ 2) n

theorem EulerPacketInduction.Stage.restricted_strain_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (t : ↑(Set.Icc 0 P.restrictedParent.T)) (x : EulerSmoothLimit.Space) : ‖(P.restrictedParent.strain.field t) x‖ ≤ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n

theorem EulerPacketInduction.Stage.restricted_curvature_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (t : ↑(Set.Icc 0 P.restrictedParent.T)) (x : EulerSmoothLimit.Space) : ‖(P.restrictedParent.curvature.field t) x‖ ≤ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.olderShear S.J S.X n