Documentation

LeanPool.NavierStokesAndEuler.Euler.PacketBudgetTimeChange

Time-endpoint equality transports the actual path norm and its profile without changing any bound.

source
def EulerPacketCylinderField.timeProfileChange {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (h : T = T') :
C(↑(Set.Icc 0 T'), ℝ)

Time profile change, given by h ▸ g.

Equations
Instances For
    source
    theorem EulerPacketCylinderField.timeProfileChange_pos {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (h : T = T') (t : ↑(Set.Icc 0 T')) :
    0 < (timeProfileChange g h) t
    source
    @[simp]
    theorem EulerPacketCylinderField.timeProfileChange_roundtrip {T T' : ℝ} (g : C(↑(Set.Icc 0 T), ℝ)) (h : T = T') :
    timeProfileChange (timeProfileChange g h) ⋯ = g
    source
    theorem EulerPacketCylinderField.Field.WordBound.changeTime {P T T' : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (h : T = T') :
    (G.changeTime h).WordBound q R A d
    source
    theorem EulerPacketCylinderField.Field.WordBound.normalized_profile_eq {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} {hT : 0 ≤ T} {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} (hG : (G.normalized hT g hg).WordBound q R A d) (g' : C(↑(Set.Icc 0 T), ℝ)) (hg' : ∀ (t : ↑(Set.Icc 0 T)), 0 < g' t) (he : g = g') :
    (G.normalized hT g' hg').WordBound q R A d
    source
    theorem EulerPacketCylinderField.Field.WordBound.normalized_changeTime {P T T' : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hG : (G.normalized hT g hg).WordBound q R A d) (h : T = T') (hT' : 0 ≤ T') (g' : C(↑(Set.Icc 0 T'), ℝ)) (hg' : ∀ (t : ↑(Set.Icc 0 T')), 0 < g' t) (he : timeProfileChange g h = g') :
    ((G.changeTime h).normalized hT' g' hg').WordBound q R A d
    source
    def EulerPacketTimeProfile.Scales.changeTime {T T' : ℝ} (S : Scales ↑(Set.Icc 0 T)) (h : T = T') :
    Scales ↑(Set.Icc 0 T')

    Change time, given by h ▸ S.

    Equations
    Instances For
      source
      @[simp]
      theorem EulerPacketTimeProfile.Scales.high_changeTime {T T' : ℝ} (S : Scales ↑(Set.Icc 0 T)) (h : T = T') (p : ℕ) :
      (S.changeTime h).high p = EulerPacketCylinderField.timeProfileChange (S.high p) h
      source
      @[simp]
      theorem EulerPacketTimeProfile.Scales.mean_changeTime {T T' : ℝ} (S : Scales ↑(Set.Icc 0 T)) (h : T = T') (p : ℕ) :
      (S.changeTime h).mean p = EulerPacketCylinderField.timeProfileChange (S.mean p) h
      source
      @[simp]
      theorem EulerPacketTimeProfile.Scales.changeTime_roundtrip {T T' : ℝ} (S : Scales ↑(Set.Icc 0 T)) (h : T = T') :
      (S.changeTime h).changeTime ⋯ = S