Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.FourierJApproximationOrthogonality

Fourier orthogonality of smooth solenoidal fields #

Compact smooth divergence-free approximants to J data have Fourier transforms orthogonal to frequency, the input condition for heat preservation.

source
def CKN.Leray.coordinateEquiv :
Foundation.Parabolic.L2Vec3 ≃L[ℝ] Foundation.Parabolic.Vec3

The canonical continuous linear equivalence between the Hilbert vector and coordinate triples.

Equations
Instances For
    source
    def CKN.Leray.coordinateToHilbertValueOrth :
    Foundation.Parabolic.Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

    The linear isometric coordinate-to-Hilbert realization used in Fourier arguments.

    Equations
    Instances For
      source
      def CKN.Leray.coordinateBasis (i : Fin 3) :
      Foundation.Parabolic.L2Vec3

      The Hilbert-space representative of the ith standard coordinate vector.

      Equations
      Instances For
        source
        noncomputable def CKN.Leray.complexCoordinateValue :
        Foundation.Parabolic.Vec3 →L[ℝ] ComplexVec3

        The real-linear map from coordinate vectors into the complexified Hilbert vector space.

        Equations
        Instances For
          source
          noncomputable def CKN.Leray.solenoidalSchwartz (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : ContDiff ℝ (↑⊤) a) (hcompact : HasCompactSupport a) :
          SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3

          The Schwartz-space representative of a smooth compactly supported coordinate field with vanishing divergence.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CKN.Leray.divergenceTraceLinear :
            (Foundation.Parabolic.L2Vec3 →L[ℝ] ComplexVec3) →ₗ[ℂ] ℂ

            The complex-linear trace that sums the diagonal derivatives of a vector-valued linear map.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem CKN.Leray.divergenceTrace_norm_bound (D : Foundation.Parabolic.L2Vec3 →L[ℝ] ComplexVec3) :
              ‖divergenceTraceLinear D‖ ≤ 3 * ‖D‖
              source
              noncomputable def CKN.Leray.divergenceTrace :
              (Foundation.Parabolic.L2Vec3 →L[ℝ] ComplexVec3) →L[ℂ] ℂ

              The continuous complex-linear extension of the diagonal derivative trace.

              Equations
              Instances For
                source
                noncomputable def CKN.Leray.schwartzDivergence (f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) :
                SchwartzMap Foundation.Parabolic.L2Vec3 ℂ

                The Schwartz function obtained by taking the divergence trace of the derivative of a vector-valued Schwartz map.

                Equations
                Instances For
                  source
                  theorem CKN.Leray.compactSolenoidal_fourierOrthogonal (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : ContDiff ℝ (↑⊤) a) (hcompact : HasCompactSupport a) (hdiv : ∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => a y i) i x = 0) (ξ : Foundation.Parabolic.L2Vec3) :
                  inner ℂ (complexifyFrequency ξ) ((FourierTransform.fourier (solenoidalSchwartz a ha hcompact)) ξ) = 0

                  Every compact smooth divergence-free vector field has a Fourier transform orthogonal to frequency.

                  source
                  theorem CKN.Leray.realVectorL2_fourierOrthogonal_of_isInJ (f : ↥RealVectorL2) (hf : IsInJ (realVectorL2Representative f)) :
                  ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), inner ℂ (complexifyFrequency ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 f)) ξ) = 0

                  Fourier orthogonality holds for the complexification of every field in the closure space J.