Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegTailsTimeIdentity

Time identities for localized regularized energy #

Compactly supported spatial weights reduce the local energy identity to a scalar weak time identity, as used in lem:reg-tails.

source
@[instance_reducible]
def CKN.Leray.regTailsTimeIdentityNormedAddCommGroup :
NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure on space-time used in the tail identity.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    noncomputable def CKN.Leray.regTailsTimeIdentityNormedSpace :
    NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

    The real normed-space structure on space-time used in the tail identity.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CKN.Leray.regTails_integrable_timeFactor_of_spatial_support (A : Foundation.Parabolic.Vec3 × ℝ → ℝ) (K : Set Foundation.Parabolic.Vec3) (hS : IsOpen (Set.univ ×ˢ Set.Ioi 0)) (hA : ContinuousOn A (Set.univ ×ˢ Set.Ioi 0)) (hK : IsCompact K) (hAzero : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 < z.2 → z.1 ∉ K → A z = 0) (η : ℝ → ℝ) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηI : tsupport η ⊆ Set.Ioi 0) :
      MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => A z * η z.2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))

      Spatial compact support and a compact positive-time factor give integrability on the positive space-time product.

      source
      theorem CKN.Leray.regTails_localEnergy_product_test (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hLE : ∀ ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), spatialGradientSq u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) z * ψ z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * J z i + 2 * p z * u z i) * spatialPartial ψ i z) (q : Foundation.Parabolic.Vec3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) (η : ℝ → ℝ) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηI : tsupport η ⊆ Set.Ioi 0) :
      have qST := fun (z : Foundation.Parabolic.ParabolicPoint) => q z.1; have A := fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * q z.1; have L := fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * ∑ i : Fin 3, spatialSecondPartial qST i i z; have V := fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * J z i + 2 * p z * u z i) * spatialPartial qST i z; 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), spatialGradientSq u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) z * q z.1 * η z.2 = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), A z * deriv η z.2 + (L z + V z) * η z.2

      The local energy identity tested against a product of compact spatial and positive time weights separates into the localized energy term and its time-independent spatial flux coefficients.

      source
      theorem CKN.Leray.regTails_laplacian_ibp_sum (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (q : Foundation.Parabolic.Vec3 → ℝ) (η : ℝ → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηI : tsupport η ⊆ Set.Ioi 0) (hUcont : ∀ (k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) k) (Set.univ ×ˢ Set.Ioi 0)) (hDcont : ∀ (k j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y k) j z) (Set.univ ×ˢ Set.Ioi 0)) (hUdiff : ∀ (k : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) k) (Set.univ ×ˢ Set.Ioi 0)) :
      ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * ∑ j : Fin 3, spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => q y.1) j j z) * η z.2 = -2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), (∑ i : Fin 3, ∑ j : Fin 3, u z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => q y.1) j z) * η z.2

      Summing the componentwise spatial integration by parts gives the cutoff Laplacian contribution to the localized energy identity.