Documentation

LeanPool.EscauriazaSereginSverak.Linear.CarlemanGaussVectorEstimate

Componentwise Gaussian conjugation #

The scalar gradient comparison from eq:carleman-gradient-pointwise is summed over the three components in prop:carleman-gauss.

source
@[instance_reducible]
def ESS.gaussVectorNormedAddCommGroup :
NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

The product norm on parabolic space-time used in this identity.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    noncomputable def ESS.gaussVectorNormedSpace :
    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_gradient_comparison (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
      Real.exp (CKN.gaussCarlemanPhase q z) ^ 2 * CKN.spatialGradientSq w (CKN.spatialGradient w) z ≤ 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)

      The scalar gradient estimate summed over a vector field's components.

      source
      theorem ESS.gauss_vector_conjugated_heat_sq (q : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.spaceTimeSet Set.univ (Set.Ioo 0 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 = Real.exp (CKN.gaussCarlemanPhase q z) ^ 2 * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2

      The sum of scalar conjugated heat energies is the weighted vector heat energy on the positive-time cylinder.

      source
      theorem ESS.gauss_vector_weighted_energy_le (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ha : 0 < a) (hw : ContDiff ℝ (↑⊤) w) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
      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) ≤ Real.exp (2 / 3) * ((a + 1) * z.2 * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase (a + 1) z) * w z i) ^ 2 + 2 * z.2 ^ 2 * (∑ i : Fin 3, CKN.scalarGradSq (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase (a + 1) y) * w y i) z + (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Real.exp (CKN.gaussCarlemanPhase (a + 1) z) * w z i) ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase (a + 1)) z))

      The original weighted field and gradient are bounded pointwise by the conjugated field energy.

      source
      theorem ESS.gauss_vector_operator_energy_le (a : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hw : ContDiff ℝ (↑⊤) w) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
      z.2 ^ 2 * ∑ i : Fin 3, CKN.carlemanConj (CKN.gaussCarlemanPhase (a + 1)) (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (CKN.gaussCarlemanPhase (a + 1) y) * w y i) z ^ 2 ≤ Real.exp (2 / 3) * (CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2)

      The conjugated heat energy is bounded by the weighted vector heat energy.