Documentation

LeanPool.NavierStokesAndEuler.Euler.MeanGradientTestSpace

The actual homogeneous first-order test space on ordinary Euclidean three-space.

source
def EulerMeanGradientTest.testSpace :
Submodule ℝ (EulerSmoothLimit.Space → EulerSmoothLimit.Space)

Smooth compactly supported vector fields, as a genuine function submodule.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev EulerMeanGradientTest.Test :
    Type

    Test: an abbreviation for ↥testSpace.

    Equations
    Instances For
      source
      theorem EulerMeanGradientTest.Test.smooth (f : Test) :
      ContDiff ℝ ↑⊤ ↑f
      source
      theorem EulerMeanGradientTest.Test.compact (f : Test) :
      HasCompactSupport ↑f
      source
      theorem EulerMeanGradientTest.Test.column_memLp (f : Test) (i : Fin 3) :
      MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => (fderiv ℝ (↑f) x) (EuclideanSpace.single i 1)) 2 MeasureTheory.volume
      source
      noncomputable def EulerMeanGradientTest.derivativeColumn (f : Test) (i : Fin 3) :
      ↥EulerMeanSolenoidal.L2

      A genuine distributional/classical derivative column as an L² vector field.

      Equations
      Instances For
        source
        theorem EulerMeanGradientTest.derivativeColumn_ae (f : Test) (i : Fin 3) :
        ↑↑(derivativeColumn f i) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => (fderiv ℝ (↑f) x) (EuclideanSpace.single i 1)
        source
        theorem EulerMeanGradientTest.derivativeColumn_add (f g : Test) (i : Fin 3) :
        derivativeColumn (f + g) i = derivativeColumn f i + derivativeColumn g i
        source
        theorem EulerMeanGradientTest.derivativeColumn_smul (c : ℝ) (f : Test) (i : Fin 3) :
        derivativeColumn (c • f) i = c • derivativeColumn f i
        source
        @[reducible, inline]
        abbrev EulerMeanGradientTest.GradientTensor :
        Type

        The Hilbert space of three L² derivative columns, with the Frobenius norm.

        Equations
        Instances For
          source
          noncomputable def EulerMeanGradientTest.testGradient :
          Test →ₗ[ℝ] GradientTensor

          The actual gradient map on compact smooth vector tests.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem EulerMeanGradientTest.testGradient_apply (f : Test) (i : Fin 3) :
            (testGradient f).ofLp i = derivativeColumn f i
            source
            theorem EulerMeanGradientTest.opNorm_le_sum_columns (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) :
            ‖A‖ ≤ ∑ i : Fin 3, ‖A (EuclideanSpace.single i 1)‖

            The operator norm is bounded by the sum of the Euclidean derivative-column norms.

            source
            theorem EulerMeanGradientTest.lpNorm_fderiv_le_gradient (f : Test) :
            MeasureTheory.lpNorm (fderiv ℝ ↑f) 2 MeasureTheory.volume ≤ 3 * ‖testGradient f‖

            The derivative norm used by the cutoff bound is controlled by the actual Hilbert gradient norm.

            source
            noncomputable def EulerMeanGradientTest.homogeneousSpace :
            Submodule ℝ GradientTensor

            Homogeneous H¹ is the closed subspace generated by actual compact test gradients.

            Equations
            Instances For
              source
              instance EulerMeanGradientTest.instCompleteSpaceSubtypeGradientTensorMemSubmoduleRealHomogeneousSpace :
              CompleteSpace ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instSubNegMonoid :
              SubNegMonoid ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instDistribSMul :
              DistribSMul ℝ ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instSMul :
              SMul ℝ ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instAddZeroClass :
              AddZeroClass ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instNorm :
              Norm ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instAddGroup :
              AddGroup ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instNormedAddCommGroup :
              NormedAddCommGroup ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instZero :
              Zero ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instMulAction :
              MulAction ℝ ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instSMulZeroClass :
              SMulZeroClass ℝ ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instMetricSpace :
              MetricSpace ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instContinuousSub :
              ContinuousSub ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instAddCommGroup :
              AddCommGroup ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instNormedSpace :
              NormedSpace ℝ ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instContinuousAdd :
              ContinuousAdd ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instSeminormedAddGroup :
              SeminormedAddGroup ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instIsUniformAddGroup :
              IsUniformAddGroup ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instSeminormedAddCommGroup :
              SeminormedAddCommGroup ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instContinuousSMul :
              ContinuousSMul ℝ ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instDistribMulAction :
              DistribMulAction ℝ ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instPseudoMetricSpace :
              PseudoMetricSpace ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instMulActionWithZero :
              MulActionWithZero ℝ ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instContinuousNeg :
              ContinuousNeg ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instTopologicalSpace :
              TopologicalSpace ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instAddCommMonoid :
              AddCommMonoid ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instIsTopologicalAddGroup :
              IsTopologicalAddGroup ↥homogeneousSpace
              source
              instance EulerMeanGradientTest.homogeneousSpace.instNormSMulClass :
              NormSMulClass ℝ ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instNeg :
              Neg ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instSMulWithZero :
              SMulWithZero ℝ ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instIsBoundedSMul :
              IsBoundedSMul ℝ ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instNormedAddGroup :
              NormedAddGroup ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instModule :
              Module ℝ ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instSub :
              Sub ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instAddMonoid :
              AddMonoid ↥homogeneousSpace
              Equations
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instUniformSpace :
              UniformSpace ↥homogeneousSpace
              Equations
              source
              instance EulerMeanGradientTest.homogeneousSpace.instContinuousConstSMul :
              ContinuousConstSMul ℝ ↥homogeneousSpace
              source
              @[reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instAdd :
              Add ↥homogeneousSpace
              Equations
              source
              @[instance_reducible]
              noncomputable instance EulerMeanGradientTest.homogeneousSpace.instInnerProductSpace :
              InnerProductSpace ℝ ↥homogeneousSpace

              Shortcut for the inner product space structure of the homogeneous space.

              Equations
              source
              noncomputable def EulerMeanGradientTest.homogeneousGradient :
              Test →ₗ[ℝ] ↥homogeneousSpace

              The dense map from genuine tests into the homogeneous Hilbert space.

              Equations
              Instances For
                source
                theorem EulerMeanGradientTest.homogeneousGradient_dense :
                DenseRange ⇑homogeneousGradient