Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Parabolic.Morrey.Kernel

Parabolic Riesz kernels #

The definitions in this module use the parabolic gauge appearing in the potential estimates and expose the dyadic shell geometry used by later integral estimates.

source
noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicRho₂ (z w : ParabolicPoint) :
ℝ

The parabolic gauge used by the order-β Riesz kernel.

Equations
Instances For
    source
    noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicRieszKernel (β : ℝ) (z w : ParabolicPoint) :
    ENNReal

    The order-β parabolic Riesz kernel as an extended nonnegative function.

    Equations
    Instances For
      source
      noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential (β : ℝ) (f : ParabolicPoint → ℝ) (z : ParabolicPoint) :
      ENNReal

      The nonnegative parabolic Riesz potential.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CKN.Foundation.Parabolic.Morrey.parabolicRieszShell (R : ℝ) (k : ℤ) (z : ParabolicPoint) :
        Set ParabolicPoint

        The shell with inner radius 2^k R and outer radius 2^(k+1) R.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem CKN.Foundation.Parabolic.Morrey.measurable_parabolicRho₂ (z : ParabolicPoint) :
          Measurable fun (w : ParabolicPoint) => parabolicRho₂ z w
          source
          theorem CKN.Foundation.Parabolic.Morrey.measurableSet_parabolicRieszShell (R : ℝ) (k : ℤ) (z : ParabolicPoint) :
          MeasurableSet (parabolicRieszShell R k z)
          source
          theorem CKN.Foundation.Parabolic.Morrey.parabolicRho₂_nonneg (z w : ParabolicPoint) :
          0 ≤ parabolicRho₂ z w
          source
          theorem CKN.Foundation.Parabolic.Morrey.parabolicDist_le_parabolicRho₂ (z w : ParabolicPoint) :
          parabolicDist z w ≤ parabolicRho₂ z w
          source
          theorem CKN.Foundation.Parabolic.Morrey.parabolicRho₂_lt_subset_metricBall {z : ParabolicPoint} {R : ℝ} :
          {w : ParabolicPoint | parabolicRho₂ z w < R} ⊆ Metric.ball z R
          source
          theorem CKN.Foundation.Parabolic.Morrey.volume_parabolicRho₂_lt_le {z : ParabolicPoint} {R : ℝ} (hR : 0 < R) :
          MeasureTheory.volume {w : ParabolicPoint | parabolicRho₂ z w < R} ≤ ENNReal.ofReal (2 ^ 5) * ENNReal.ofReal (R ^ 5) * MeasureTheory.volume (parabolicCylinder 0 0 1)
          source
          theorem CKN.Foundation.Parabolic.Morrey.volume_parabolicRieszShell_le {z : ParabolicPoint} {R : ℝ} {k : ℤ} (hR : 0 < R) :
          MeasureTheory.volume (parabolicRieszShell R k z) ≤ ENNReal.ofReal (2 ^ 5) * ENNReal.ofReal ((2 ^ (↑k + 1) * R) ^ 5) * MeasureTheory.volume (parabolicCylinder 0 0 1)
          source
          theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszKernel_nonneg (β : ℝ) (z w : ParabolicPoint) :
          0 ≤ parabolicRieszKernel β z w
          source
          theorem CKN.Foundation.Parabolic.Morrey.mem_parabolicRieszShell {R : ℝ} {k : ℤ} {z w : ParabolicPoint} (hinner : 2 ^ ↑k * R ≤ parabolicRho₂ z w) (houter : parabolicRho₂ z w < 2 ^ (↑k + 1) * R) :
          w ∈ parabolicRieszShell R k z
          source
          theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszShell_subset_tail {R : ℝ} {k : ℤ} {z : ParabolicPoint} (hR : 0 < R) (hk : 0 ≤ k) :
          parabolicRieszShell R k z ⊆ {w : ParabolicPoint | R ≤ parabolicRho₂ z w}
          source
          theorem CKN.Foundation.Parabolic.Morrey.exists_shell_of_pos_lt {z w : ParabolicPoint} {R : ℝ} (hR : 0 < R) (hρ : 0 < parabolicRho₂ z w) (hρR : parabolicRho₂ z w < R) :
          ∃ k < 0, w ∈ parabolicRieszShell R k z

          A positive point below a radius belongs to a negative dyadic shell.

          source
          theorem CKN.Foundation.Parabolic.Morrey.parabolicRho₂_zero_subset_singleton (z : ParabolicPoint) :
          {w : ParabolicPoint | parabolicRho₂ z w = 0} ⊆ {z}

          The zero set of the gauge is contained in its center.

          source
          theorem CKN.Foundation.Parabolic.Morrey.shell_power_identity {a β : ℝ} (ha : 0 < a) (hβ : 0 ≤ β) :
          β ≤ 5 → ENNReal.ofReal a ^ (-(5 - β)) * ENNReal.ofReal ((2 * a) ^ 5) = ENNReal.ofReal (2 ^ 5) * ENNReal.ofReal (a ^ β)

          The kernel-volume scaling identity on a dyadic shell.

          source
          def CKN.Foundation.Parabolic.Morrey.negativeShell (R : ℝ) (n : ℕ) (z : ParabolicPoint) :
          Set ParabolicPoint

          Dyadic parabolic shell strictly below the reference scale.

          Equations
          Instances For
            source
            noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicLocalKernelConstant (β : ℝ) :
            ENNReal

            The geometric constant used by the local kernel estimate.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszKernel_local_le {β : ℝ} (hβ : 0 < β) (hβ5 : β < 5) {R : ℝ} (hR : 0 < R) (z : ParabolicPoint) :
              ∫⁻ (w : ParabolicPoint) in {w : ParabolicPoint | parabolicRho₂ z w < R}, parabolicRieszKernel β z w ≤ parabolicLocalKernelConstant β * ENNReal.ofReal (R ^ β)
              source
              theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_mono {β : ℝ} {f g : ParabolicPoint → ℝ} (hfg : ∀ (w : ParabolicPoint), |f w| ≤ |g w|) (z : ParabolicPoint) :
              parabolicRieszPotential β f z ≤ parabolicRieszPotential β g z