Documentation

LeanPool.NavierStokesAndEuler.Euler.PacketKnownPieceScales

Uniform shifts and actual time profiles for the three known pieces of every grade.

def EulerPacketCylinderField.KnownPiece.shift (k : KnownPiece) (i : ℕ) :

Shift as an element of ℕ.

Equations

Instances For

def EulerPacketCylinderField.KnownPiece.profile {K : Type u_1} [TopologicalSpace K] (k : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i : ℕ) :

Profile as an element of C(K,ℝ).

Equations

EulerPacketCylinderField.KnownPiece.high.profile S i = S.high i
EulerPacketCylinderField.KnownPiece.mean.profile S i = S.mean i
EulerPacketCylinderField.KnownPiece.corrector.profile S i = S.high (i - 1)

Instances For

def EulerPacketCylinderField.KnownPiece.envelope {K : Type u_1} [TopologicalSpace K] (k : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i : ℕ) :

Envelope as an element of C(K,ℝ).

Equations

EulerPacketCylinderField.KnownPiece.high.envelope S i = S.high i
EulerPacketCylinderField.KnownPiece.corrector.envelope S i = S.high i
EulerPacketCylinderField.KnownPiece.mean.envelope S i = S.mean i

Instances For

theorem EulerPacketCylinderField.KnownPiece.profile_pos {K : Type u_1} [TopologicalSpace K] (k : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i : ℕ) (t : K) :

0 < (k.profile S i) t

theorem EulerPacketCylinderField.KnownPiece.envelope_pos {K : Type u_1} [TopologicalSpace K] (k : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i : ℕ) (t : K) :

0 < (k.envelope S i) t

theorem EulerPacketCylinderField.KnownPiece.profile_le_envelope {K : Type u_1} [TopologicalSpace K] (k : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i : ℕ) (t : K) :

(k.profile S i) t ≤ (k.envelope S i) t

theorem EulerPacketCylinderField.KnownPiece.profile_le_high {K : Type u_1} [TopologicalSpace K] (k : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i : ℕ) (hk : k ≠ mean) (t : K) :

(k.profile S i) t ≤ (S.high i) t

theorem EulerPacketCylinderField.KnownPiece.active_one_le (k : KnownPiece) (p i : ℕ) (hi : k.active p i) :

1 ≤ i

theorem EulerPacketCylinderField.KnownPiece.shift_le_high (k : KnownPiece) (i : ℕ) :

k.shift i ≤ EulerPacketShiftArithmetic.highShift i

theorem EulerPacketCylinderField.KnownPiece.slow_shift_room (k l : KnownPiece) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hij : i + j = p) :

k.shift i + l.shift j + 1 < EulerPacketShiftArithmetic.meanForceShift p

theorem EulerPacketCylinderField.KnownPiece.slow_shift_room_high (k l : KnownPiece) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hij : i + j = p) :

k.shift i + l.shift j + 1 < EulerPacketShiftArithmetic.highForceShift p

theorem EulerPacketCylinderField.KnownPiece.fast_mean_shift_room (l : KnownPiece) (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hij : i + j = p + 1) :

mean.shift i + l.shift j + 1 < EulerPacketShiftArithmetic.highForceShift p

theorem EulerPacketCylinderField.KnownPiece.fast_corrector_shift_room (l : KnownPiece) (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hij : i + j = p + 1) :

corrector.shift i + l.shift j + 1 < EulerPacketShiftArithmetic.meanForceShift p

theorem EulerPacketCylinderField.KnownPiece.slow_profile_mean {K : Type u_1} [TopologicalSpace K] (k l : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hij : i + j = p) (t : K) :

(k.profile S i) t * (l.profile S j) t ≤ (S.mean p) t

theorem EulerPacketCylinderField.KnownPiece.slow_profile_high {K : Type u_1} [TopologicalSpace K] (k l : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hij : i + j = p) (hhigh : ¬(k = mean ∧ l = mean)) (t : K) :

(k.profile S i) t * (l.profile S j) t ≤ (S.high p) t

theorem EulerPacketCylinderField.KnownPiece.fast_mean_profile_high {K : Type u_1} [TopologicalSpace K] (l : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i j p : ℕ) (hl : l ≠ mean) (hi : 1 ≤ i) (hj : 1 ≤ j) (hij : i + j = p + 1) (t : K) :

(mean.profile S i) t * (l.profile S j) t ≤ (S.high p) t

theorem EulerPacketCylinderField.KnownPiece.fast_corrector_profile_mean {K : Type u_1} [TopologicalSpace K] (l : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i j p : ℕ) (hl : l ≠ mean) (hi : 2 ≤ i) (hj : 1 ≤ j) (hij : i + j = p + 1) (t : K) :

(corrector.profile S i) t * (l.profile S j) t ≤ (S.mean p) t

theorem EulerPacketCylinderField.KnownPiece.fast_corrector_profile_high {K : Type u_1} [TopologicalSpace K] (l : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i j p : ℕ) (hl : l ≠ mean) (hi : 2 ≤ i) (hj : 1 ≤ j) (hij : i + j = p + 1) (t : K) :

(corrector.profile S i) t * (l.profile S j) t ≤ (S.high p) t