Documentation

LeanPool.EscauriazaSereginSverak.Linear.CarlemanGaussVectorIntegrable

Integrability of the Gaussian vector energy #

Compact support inside the positive-time cylinder makes the original weighted energy integrable despite the singular expression at time zero.

source
@[instance_reducible]
noncomputable def ESS.gaussVectorIntegrableMeasureSpace :
MeasureTheory.MeasureSpace CKN.Foundation.Parabolic.ParabolicPoint

Product Lebesgue measure on parabolic space-time.

Equations
Instances For
    source
    @[instance_reducible]
    def ESS.gaussVectorIntegrableNormedAddCommGroup :
    NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

    The product norm on parabolic space-time used for classical differentiation.

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

      The real scalar action compatible with the product norm on parabolic space-time.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem ESS.gauss_vector_norm_sq_smooth_support (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) :
        (ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) ∧ (HasCompactSupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) ∧ (tsupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) ⊆ tsupport w

        The squared norm of a smooth compactly supported vector field is smooth and supported where the field is supported.

        source
        theorem ESS.gauss_vector_gradient_sq_smooth_support (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) :
        (ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq w (CKN.spatialGradient w) z) ∧ (HasCompactSupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq w (CKN.spatialGradient w) z) ∧ (tsupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq w (CKN.spatialGradient w) z) ⊆ tsupport w

        The squared spatial gradient of a smooth compactly supported vector field has the same support property.

        source
        theorem ESS.gauss_original_energy_integrable (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
        MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z)) MeasureTheory.volume

        The original weighted energy in prop:carleman-gauss is integrable.

        source
        theorem ESS.gauss_conjugated_component_properties (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (i : Fin 3) :
        (ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ∧ (HasCompactSupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ∧ (tsupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)

        Each exponentially conjugated component is smooth, compactly supported, and supported inside the positive-time cylinder.

        source
        theorem ESS.gauss_vector_upper_integral_eq_sum (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
        ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), q * z.2 * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ^ 2 + 2 * z.2 ^ 2 * (∑ i : Fin 3, CKN.scalarGradSq (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z + (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z) = ∑ i : Fin 3, ((q * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.2 * (Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ^ 2) + 2 * ((∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.2 ^ 2 * CKN.scalarGradSq (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z) + ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.2 ^ 2 * (Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z))

        The vector expression produced by the Gaussian gradient comparison is integrable, and its integral splits into scalar component energies.

        source
        theorem ESS.gauss_vector_upper_integrable (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
        MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => q * z.2 * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ^ 2 + 2 * z.2 ^ 2 * (∑ i : Fin 3, CKN.scalarGradSq (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z + (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase q z) * w z i) ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z)) MeasureTheory.volume

        The vector energy after exponential conjugation is integrable.

        source
        theorem ESS.gauss_vector_conjugated_heat_integral_eq_sum (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
        ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * ∑ i : Fin 3, CKN.carlemanConj (CKN.gaussCarlemanPhase q) (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z ^ 2 = ∑ i : Fin 3, ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * CKN.carlemanConj (CKN.gaussCarlemanPhase q) (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase q y) * w y i) z ^ 2

        The conjugated vector heat integral splits into the three scalar heat integrals.