Documentation

LeanPool.EscauriazaSereginSverak.Linear.CarlemanGaussIntegrated

Integrated Gaussian gradient estimate #

The Gaussian phase specializes eq:carleman-gradient-integrated to the coefficient bound used in eq:carleman-E.

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

Product Lebesgue measure on parabolic space-time.

Equations
Instances For
    source
    @[instance_reducible]
    def ESS.gaussIntegratedNormedAddCommGroup :
    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.gaussIntegratedNormedSpace :
      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_scalar_gradient_energy_le (q : ℝ) (hq : 1 ≤ q) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) :
        (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * CKN.scalarGradSq v z) + ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * v z ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z ≤ (3 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), q / 3 * z.2 * v z ^ 2) + |∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * v z * CKN.carlemanConj (CKN.gaussCarlemanPhase q) v z|

        The integrated gradient and phase-gradient energy is bounded by three times the Gaussian commutator mass and the cross integral.

        source
        theorem ESS.gauss_scalar_energy_le_of_commutator (q : ℝ) (hq : 1 ≤ q) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ContDiff ℝ (↑⊤) v) (hvc : HasCompactSupport v) (hvU : tsupport v ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (hP : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => z.2 ^ 2 * CKN.carlemanConj (CKN.gaussCarlemanPhase q) v z ^ 2) MeasureTheory.volume) (hIP : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), q / 3 * z.2 * v z ^ 2 ≤ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * CKN.carlemanConj (CKN.gaussCarlemanPhase q) v z ^ 2) :
        (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * CKN.scalarGradSq v z) + ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * v z ^ 2 * CKN.scalarGradSq (CKN.gaussCarlemanPhase q) z ≤ (3 + √6) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ^ 2 * CKN.carlemanConj (CKN.gaussCarlemanPhase q) v z ^ 2

        The Gaussian commutator inequality and the cross estimate control the scalar gradient and phase-gradient energy.