Documentation

LeanPool.NavierStokesAndEuler.Euler.PacketKnownDecomposition

Exact finite A/B/C decomposition of the known force. The only fast products retained are BA, BC, CA and CC. This is raw algebra on the actual sliced jets.

source
theorem EulerPacketCylinderField.sum_knownPiece {E : Type u_1} [AddCommMonoid E] (f : KnownPiece → E) :
∑ k : KnownPiece, f k = f KnownPiece.high + f KnownPiece.mean + f KnownPiece.corrector
source
inductive EulerPacketCylinderField.KnownTerm :
Type

Fifteen named summand kinds before the final new-mean/primary interaction.

Instances For
    source
    @[instance_reducible]
    instance EulerPacketCylinderField.instDecidableEqKnownTerm :
    DecidableEq KnownTerm
    Equations
    source
    def EulerPacketCylinderField.instDecidableEqKnownTerm.decEq (x✝ x✝¹ : KnownTerm) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance EulerPacketCylinderField.instFintypeKnownTerm :
      Fintype KnownTerm
      Equations
      • One or more equations did not get rendered due to their size.
      source
      theorem EulerPacketCylinderField.card_knownTerm :
      Fintype.card KnownTerm = 15
      source
      theorem EulerPacketCylinderField.sum_knownTerm {E : Type u_1} [AddCommMonoid E] (f : KnownTerm → E) :
      ∑ k : KnownTerm, f k = f KnownTerm.previousLinear + f KnownTerm.previousPressure + ∑ l : KnownPiece, ∑ r : KnownPiece, f (KnownTerm.slow l r) + f KnownTerm.fastMeanHigh + f KnownTerm.fastMeanCorrector + f KnownTerm.fastCorrectorHigh + f KnownTerm.fastCorrectorCorrector
      source
      noncomputable def EulerPacketCylinderField.KnownTerm.raw (k : KnownTerm) (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (i j : ℕ) :
      EulerPacketProfileRecursion.VectorField

      Raw as an element of VectorField.

      Equations
      Instances For
        source
        def EulerPacketCylinderField.KnownTerm.zeroMean (k : KnownTerm) :
        Bool

        These two families have zero angular mean by periodicity.

        Equations
        Instances For
          source
          def EulerPacketCylinderField.KnownTerm.meanOnly (k : KnownTerm) :
          Bool

          The pure mean slow product is constant in angle.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev EulerPacketCylinderField.KnownTermIndex :
            Type

            Known term index: an abbreviation for KnownTerm × (ℕ × ℕ).

            Equations
            Instances For
              source
              def EulerPacketCylinderField.knownTermIndices (p : ℕ) :
              Finset KnownTermIndex

              Known term indices, given by Finset.univ.product ((Finset.range (p+2)).product (Finset.range (p+2))).

              Equations
              Instances For
                source
                theorem EulerPacketCylinderField.knownTermIndices_card (p : ℕ) :
                (knownTermIndices p).card = 15 * (p + 2) ^ 2
                source
                theorem EulerPacketCylinderField.knownTermIndices_card_room (p : ℕ) :
                (knownTermIndices p).card + 1 ≤ 100 * (p + 2) ^ 2
                source
                theorem EulerPacketCylinderField.sum_knownTerm_raw (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (z : EulerPacketPointJets.Domain) :
                ∑ q ∈ knownTermIndices p, q.1.raw O p a q.2.1 q.2.2 z = (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (a (p - 1)).corrector z) + (EulerPacketPointJets.slowPressure (O.inverseFrame z)) (EulerPacketPointJets.pressureJet (a (p - 1)).highPressure z) + ∑ l : KnownPiece, ∑ r : KnownPiece, EulerFiniteGrades.convolution (p + 1) (EulerPacketPointJets.slowAdvection (O.inverseFrame z)) (l.jet O p a z) (r.jet O p a z) p + EulerFiniteGrades.convolution (p + 1) (EulerPacketPointJets.fastAdvection (O.normal z)) (KnownPiece.mean.jet O p a z) (KnownPiece.high.jet O p a z) (p + 1) + EulerFiniteGrades.convolution (p + 1) (EulerPacketPointJets.fastAdvection (O.normal z)) (KnownPiece.mean.jet O p a z) (KnownPiece.corrector.jet O p a z) (p + 1) + EulerFiniteGrades.convolution (p + 1) (EulerPacketPointJets.fastAdvection (O.normal z)) (KnownPiece.corrector.jet O p a z) (KnownPiece.high.jet O p a z) (p + 1) + EulerFiniteGrades.convolution (p + 1) (EulerPacketPointJets.fastAdvection (O.normal z)) (KnownPiece.corrector.jet O p a z) (KnownPiece.corrector.jet O p a z) (p + 1)
                source
                theorem EulerPacketCylinderField.knownForce_eq_term_sum (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (hp : 2 ≤ p) (a : ℕ → EulerPacketProfileRecursion.Profile) (hc : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (z : EulerPacketPointJets.Domain) (ha : ∀ (i : ℕ), inner ℝ (O.normal z) (KnownPiece.high.jet O p a z i).1 = 0) (hb : ∀ (i : ℕ), (KnownPiece.mean.jet O p a z i).2 EulerPacketPointJets.angleDirection = 0) :
                EulerPacketProfileRecursion.knownForce O p a z = -∑ q ∈ knownTermIndices p, q.1.raw O p a q.2.1 q.2.2 z

                Exact raw known force, with all identically zero fast interactions removed.