LeanPool.NavierStokesAndEuler.Euler.PacketStageInputs

Actual packet inputs at every finite stage, together with the source-only parameter cap and the chosen frequency guard.

The zero-history normal stage has the same fixed parameter envelope as every positive-history stage. Its actual initial coordinate has norm one.

source

theorem EulerParentPacketFrames.LabelData.forwardNormalParameterSize_bound {A : Parent} (L : LabelData A) (H : LowBounds A) {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 : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R support hsupport) 0) (G : EulerPacketSourceGeometry.ForwardGuards P) (J D : ℕ) (hJ : 2 ≤ J) (C X : ℝ) (hC : 1 ≤ C) (hX : 1 ≤ X) (n : ℕ) (Ti : ℝ) (hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7)) (hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4)) (hK : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ 80) (hTi : Ti ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X) (hBc : H.Bc ≤ EulerPacketLowConstants.gradientConstant * X ^ 1000 + 2) (hL : H.L = EulerMeanHarmonic.boundaryLocalizationC1 * H.Bc + 1) (hΘ : P.horizon ≤ EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n) (hδ : G.δ = EulerPacketSourceScaleSequence.spike J X n) (hh : G.hchild = EulerPacketSourceScaleSequence.shear J X n) (hshear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n) :

L.geometryForwardParameterSize H m hm R support hsupport P G Ti G.initialCoordinate ≤ EulerNormalPacketParameters.envelope J C X n

source

theorem EulerParentPacketFrames.GeometryForwardInput.parameterSize_one {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) :

1 ≤ I.parameterSize

source

noncomputable def EulerPacketInduction.Stage.joinedInput {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

EulerPacketInitial.Input ↥(EulerTransverseFrameCoordinates.referencePlane (P.joinedNormal hn))

Joined input, bundling parent, label, low, normal and the required compatibility proofs.

Equations

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

Instances For

source

@[simp]

theorem EulerPacketInduction.Stage.joinedInput_parent {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).parent = P.restrictedParent

source

@[simp]

theorem EulerPacketInduction.Stage.joinedInput_label {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).label = P.restrictedState.labels

source

@[simp]

theorem EulerPacketInduction.Stage.joinedInput_low {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).low = P.restrictedLow

source

@[simp]

theorem EulerPacketInduction.Stage.joinedInput_frame {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).frame = P.joinedFrame hn

source

@[simp]

theorem EulerPacketInduction.Stage.joinedInput_geometry {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).geometry = P.joinedGuards hn hq hB

source

@[simp]

theorem EulerPacketInduction.Stage.joinedInput_terminal {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).terminal = EulerPacketSourceGeometry.Guards.terminal ⋯ ⋯ (P.joinedFrame hn) (P.joinedHistory hn) (P.joinedGuards hn hq hB)

source

theorem EulerPacketInduction.Stage.joinedInput_parameterSize {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).parameterSize ≤ EulerNormalPacketParameters.envelope S.J 4 S.X n

source

theorem EulerPacketInduction.Stage.joinedInput_frequency {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).frequencyGuard (EulerPacketSourceScaleSequence.frequency S.J S.X n)

source

theorem EulerPacketInduction.Stage.joinedInput_targetTime {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

((P.joinedInput hn hq hB).geometry.lowGeometry ⋯).targetTime = P.nextTime

source

theorem EulerPacketInduction.Stage.joinedInput_sigma_bound {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence S.J S.X n ≤ 2

source

theorem EulerPacketInduction.Stage.joinedInput_scale {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.joinedInput hn hq hB).parent.ell = EulerPacketSourceScaleSequence.supportScale S.J S.X n

source

noncomputable def EulerPacketInduction.Stage.forwardInput {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

EulerParentPacketFrames.GeometryForwardInput ↥(EulerTransverseFrameCoordinates.referencePlane P.forwardNormal)

Forward input, bundling parent, label, low, normal and the required compatibility proofs.

Equations

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

Instances For

source

@[simp]

theorem EulerPacketInduction.Stage.forwardInput_parent {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).parent = P.restrictedParent

source

@[simp]

theorem EulerPacketInduction.Stage.forwardInput_label {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).label = P.restrictedState.labels

source

@[simp]

theorem EulerPacketInduction.Stage.forwardInput_low {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).low = P.restrictedLow

source

@[simp]

theorem EulerPacketInduction.Stage.forwardInput_frame {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).frame = P.forwardFrame

source

@[simp]

theorem EulerPacketInduction.Stage.forwardInput_geometry {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).geometry = P.forwardGuards hq hB

source

theorem EulerPacketInduction.Stage.forwardInput_parameterSize {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).parameterSize ≤ EulerNormalPacketParameters.envelope S.J 4 S.X 0

source

theorem EulerPacketInduction.Stage.forwardInput_frequency {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).frequencyGuard (EulerPacketSourceScaleSequence.frequency S.J S.X 0)

source

theorem EulerPacketInduction.Stage.forwardInput_targetTime {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

((P.forwardInput hq hB).geometry.lowGeometry ⋯).targetTime = P.nextTime

source

theorem EulerPacketInduction.Stage.forwardInput_sigma_bound {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence S.J S.X 0 ≤ 2

source

theorem EulerPacketInduction.Stage.forwardInput_scale {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) :

(P.forwardInput hq hB).parent.ell = EulerPacketSourceScaleSequence.supportScale S.J S.X 0