Documentation

LeanPool.NavierStokesAndEuler.Euler.Foundations.VectorCalculus

Vector Calculus #

source
noncomputable def EulerVectorCalculus.partialDerivative (f : EulerSmoothLimit.Space → ℝ) (i : Fin 3) (x : EulerSmoothLimit.Space) :
ℝ

The ordinary coordinate derivative, evaluated using the Fréchet derivative.

Equations
Instances For
    source
    noncomputable def EulerVectorCalculus.curl (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) :
    EulerSmoothLimit.Space

    The three-dimensional curl of a vector potential in standard coordinates.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem EulerVectorCalculus.curl_apply (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) (i : Fin 3) :
      (curl ψ x).ofLp i = partialDerivative (ψ (i + 2)) (i + 1) x - partialDerivative (ψ (i + 1)) (i + 2) x
      source
      theorem EulerVectorCalculus.contDiff_partialDerivative (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) :
      ContDiff ℝ (↑⊤) (partialDerivative f i)
      source
      theorem EulerVectorCalculus.contDiff_curl (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (hψ : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (ψ i)) :
      ContDiff ℝ (↑⊤) (curl ψ)
      source
      theorem EulerVectorCalculus.partialDerivative_comm (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ 2 f) (i j : Fin 3) (x : EulerSmoothLimit.Space) :
      partialDerivative (partialDerivative f i) j x = partialDerivative (partialDerivative f j) i x
      source
      theorem EulerVectorCalculus.fderiv_coordinate (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hf : DifferentiableAt ℝ f x) (i : Fin 3) (v : EulerSmoothLimit.Space) :
      (fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (f y).ofLp i) x) v = ((fderiv ℝ f x) v).ofLp i
      source
      theorem EulerVectorCalculus.divergence_curl (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (hψ : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (ψ i)) (x : EulerSmoothLimit.Space) :
      EulerSmoothLimit.divergence (curl ψ) x = 0
      source
      theorem EulerVectorCalculus.tsupport_curl_subset (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (K : Set EulerSmoothLimit.Space) (hK : IsClosed K) (hψ : ∀ (i : Fin 3), tsupport (ψ i) ⊆ K) :
      tsupport (curl ψ) ⊆ K
      source
      theorem EulerVectorCalculus.hasCompactSupport_curl (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (K : Set EulerSmoothLimit.Space) (hK : IsCompact K) (hψ : ∀ (i : Fin 3), tsupport (ψ i) ⊆ K) :
      HasCompactSupport (curl ψ)
      source
      theorem EulerVectorCalculus.partialDerivative_odd_of_even (f : EulerSmoothLimit.Space → ℝ) (hf : Differentiable ℝ f) (heven : ∀ (x : EulerSmoothLimit.Space), f (-x) = f x) (i : Fin 3) (x : EulerSmoothLimit.Space) :
      partialDerivative f i (-x) = -partialDerivative f i x
      source
      theorem EulerVectorCalculus.odd_curl_of_even (ψ : Fin 3 → EulerSmoothLimit.Space → ℝ) (hψ : ∀ (i : Fin 3), Differentiable ℝ (ψ i)) (heven : ∀ (i : Fin 3) (x : EulerSmoothLimit.Space), ψ i (-x) = ψ i x) (x : EulerSmoothLimit.Space) :
      curl ψ (-x) = -curl ψ x
      source
      noncomputable def EulerVectorCalculus.linearPotential (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) :
      ℝ

      The vector potential -x × (L x) / 3 in cyclic coordinates.

      Equations
      Instances For
        source
        theorem EulerVectorCalculus.contDiff_linearPotential (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) :
        ContDiff ℝ (↑⊤) (linearPotential L i)
        source
        theorem EulerVectorCalculus.linearPotential_even (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) :
        linearPotential L i (-x) = linearPotential L i x
        source
        theorem EulerVectorCalculus.partialDerivative_linearPotential (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (i j : Fin 3) (x : EulerSmoothLimit.Space) :
        partialDerivative (linearPotential L i) j x = -((EuclideanSpace.single j 1).ofLp (i + 1) * (L x).ofLp (i + 2) + x.ofLp (i + 1) * (L (EuclideanSpace.single j 1)).ofLp (i + 2) - ((EuclideanSpace.single j 1).ofLp (i + 2) * (L x).ofLp (i + 1) + x.ofLp (i + 2) * (L (EuclideanSpace.single j 1)).ofLp (i + 1))) / 3
        source
        theorem EulerVectorCalculus.curl_linearPotential (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) :
        curl (linearPotential L) x = L x - ((LinearMap.trace ℝ EulerSmoothLimit.Space) ↑L / 3) • x
        source
        theorem EulerVectorCalculus.curl_linearPotential_of_trace_zero (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : (LinearMap.trace ℝ EulerSmoothLimit.Space) ↑L = 0) (x : EulerSmoothLimit.Space) :
        curl (linearPotential L) x = L x
        source
        theorem EulerVectorCalculus.curl_congr_nhds (ψ φ : Fin 3 → EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) (h : ∀ (i : Fin 3), ψ i =ᶠ[nhds x] φ i) :
        curl ψ x = curl φ x
        source
        theorem EulerVectorCalculus.compact_solenoidal_extension (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : (LinearMap.trace ℝ EulerSmoothLimit.Space) ↑L = 0) (r R : ℝ) (hr : 0 < r) (hrR : r < R) :
        ∃ (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space), ContDiff ℝ (↑⊤) u ∧ HasCompactSupport u ∧ tsupport u ⊆ Metric.closedBall 0 R ∧ (∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) ∧ (∀ (x : EulerSmoothLimit.Space), u (-x) = -u x) ∧ ∀ x ∈ Metric.ball 0 r, u x = L x

        A trace-free linear velocity has an odd, smooth, compactly supported, divergence-free extension from any prescribed ball.