Documentation

LeanPool.NavierStokesAndEuler.Euler.AngleMeanZeroPrimitive

The actual mean-zero periodic angular primitive #

This is an explicit Bochner integral, valid also for a Hilbert-valued angle curve such as a time-L² pressure coefficient. Periodicity is proved from the zero integral of the forcing; subtracting the actual mean fixes the constant.

source
noncomputable def EulerAngleMeanZeroPrimitive.rawPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (θ : ℝ) :
E

The raw angular primitive, anchored at angle zero.

Equations
Instances For
    source
    noncomputable def EulerAngleMeanZeroPrimitive.primitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : ℝ) (f : ℝ → E) (θ : ℝ) :
    E

    The actual angular primitive with its mean over one period removed.

    Equations
    Instances For
      source
      theorem EulerAngleMeanZeroPrimitive.rawPrimitive_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ℝ → E) (hf : Continuous f) (θ : ℝ) :
      HasDerivAt (rawPrimitive f) (f θ) θ

      The explicit integral has the actual derivative prescribed by the forcing.

      source
      theorem EulerAngleMeanZeroPrimitive.rawPrimitive_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ℝ → E) (hf : Continuous f) :
      Continuous (rawPrimitive f)

      The raw angular primitive is continuous.

      source
      theorem EulerAngleMeanZeroPrimitive.primitive_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P : ℝ) (f : ℝ → E) (hf : Continuous f) (θ : ℝ) :
      HasDerivAt (primitive P f) (f θ) θ

      Removing the mean does not change the actual angular derivative.

      source
      theorem EulerAngleMeanZeroPrimitive.primitive_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P : ℝ) (f : ℝ → E) (hf : Continuous f) :
      Continuous (primitive P f)

      The normalized angular primitive is continuous.

      source
      theorem EulerAngleMeanZeroPrimitive.rawPrimitive_periodic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : ℝ) (f : ℝ → E) (hf : Continuous f) (hper : Function.Periodic f P) (hmean : ∫ (θ : ℝ) in 0..P, f θ = 0) :
      Function.Periodic (rawPrimitive f) P

      Zero angular mean of the forcing makes the raw integral periodic.

      source
      theorem EulerAngleMeanZeroPrimitive.primitive_periodic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : ℝ) (f : ℝ → E) (hf : Continuous f) (hper : Function.Periodic f P) (hmean : ∫ (θ : ℝ) in 0..P, f θ = 0) :
      Function.Periodic (primitive P f) P

      The normalized angular primitive is genuinely periodic.

      source
      theorem EulerAngleMeanZeroPrimitive.primitive_mean_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P : ℝ) (hP : P ≠ 0) (f : ℝ → E) (hf : Continuous f) :
      ∫ (θ : ℝ) in 0..P, primitive P f θ = 0

      The normalization gives exactly zero integral over one angular period.

      source
      theorem EulerAngleMeanZeroPrimitive.primitive_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P : ℝ) (hP : P ≠ 0) (f : ℝ → E) (hf : Continuous f) (g : ℝ → E) (hg : ∀ (θ : ℝ), HasDerivAt g (f θ) θ) (hmean : ∫ (θ : ℝ) in 0..P, g θ = 0) :
      g = primitive P f

      The zero-mean angular primitive is unique among genuine differentiable primitives.