Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.DyadicCells

Dyadic cells for the short-time layer #

The cells partition each slab ℝ³ × (2⁻ᵏ/2, 2⁻ᵏ) up to null grid times. The spatial cubes are half-open and the time intervals are open, as in lem:bu-small-time of the Escauriaza–Seregin–Šverák manuscript.

source
noncomputable def CKN.Foundation.buSmallTimeDyadicScale (k : ℤ) :
ℝ

The time scale of the kth dyadic layer.

Equations
Instances For
    source
    noncomputable def CKN.Foundation.buSmallTimeDyadicSide (k : ℤ) :
    ℝ

    The spatial side length of each cell in the kth layer.

    Equations
    Instances For
      source
      noncomputable def CKN.Foundation.buSmallTimeDyadicTimeLength (k : ℤ) :
      ℝ

      The time length of each cell in the kth layer.

      Equations
      Instances For
        source
        noncomputable def CKN.Foundation.buSmallTimeDyadicTimeBoundary (k : ℤ) (n : ℕ) :
        ℝ

        A time-grid point in the kth layer.

        Equations
        Instances For
          source
          def CKN.Foundation.buSmallTimeDyadicSpatialCell (k : ℤ) (m : Fin 3 → ℤ) :
          Set Parabolic.Vec3

          The spatial cube indexed by the integer lattice point m.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CKN.Foundation.buSmallTimeDyadicTimeCell (k : ℤ) (ell : Fin 2048) :
            Set ℝ

            The open time interval indexed by ell.

            Equations
            Instances For
              source
              def CKN.Foundation.buSmallTimeDyadicCell (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) :
              Set Parabolic.ParabolicPoint

              A dyadic space-time cell in the kth short-time layer.

              Equations
              Instances For
                source
                noncomputable def CKN.Foundation.buSmallTimeDyadicCellCenter (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) :
                Parabolic.ParabolicPoint

                The spatial and temporal midpoint of a dyadic cell.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem CKN.Foundation.buSmallTimeDyadicScale_pos (k : ℤ) :
                  0 < buSmallTimeDyadicScale k

                  The dyadic time scale is positive.

                  source
                  theorem CKN.Foundation.buSmallTimeDyadicSide_pos (k : ℤ) :
                  0 < buSmallTimeDyadicSide k

                  The spatial side length of each cell is positive.

                  source
                  theorem CKN.Foundation.buSmallTimeDyadicTimeLength_pos (k : ℤ) :
                  0 < buSmallTimeDyadicTimeLength k

                  The time length of each cell is positive.

                  source
                  theorem CKN.Foundation.buSmallTimeDyadicCell_subset_layer (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) :
                  buSmallTimeDyadicCell k m ell ⊆ Set.univ ×ˢ Set.Ioo (buSmallTimeDyadicScale k / 2) (buSmallTimeDyadicScale k)

                  Every cell is contained in the dyadic time slab it partitions.

                  source
                  theorem CKN.Foundation.buSmallTimeDyadicCell_spatial_distance_le (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : Parabolic.ParabolicPoint) (hz : z ∈ buSmallTimeDyadicCell k m ell) :
                  Parabolic.vec3EuclideanNorm (z.1 - (buSmallTimeDyadicCellCenter k m ell).1) ≤ √3 * buSmallTimeDyadicSide k

                  The spatial displacement of a point in a cell from its center is bounded by √3 times the spatial side length.

                  source
                  theorem CKN.Foundation.buSmallTimeDyadicCell_lintegral_eq_tsum (k : ℤ) (f : Parabolic.ParabolicPoint → ENNReal) :
                  ∫⁻ (z : Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo (buSmallTimeDyadicScale k / 2) (buSmallTimeDyadicScale k), f z = ∑' (ij : (Fin 3 → ℤ) × Fin 2048), ∫⁻ (z : Parabolic.ParabolicPoint) in buSmallTimeDyadicCell k ij.1 ij.2, f z

                  The dyadic cells partition the layer for integration of nonnegative data.