OAI/Geometry/RCD/Coordinates/RegularMassMatrices.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Canonical mean and local mass matrices of the constructed neighborhood

  1. def OAI.RegularPointCoordinates.RegularBilinearData.meanAt line 25

    Source documentation

    The actual dyadic mean Gram, using an already constructed exact frame only to certify its invertibility.

    def meanAt (i : ℕ) : Euclidean n ≃L[ℝ] Euclidean n :=
…

    Mentions: OAI.RegularPointCoordinates.Euclidean

  2. theorem OAI.RegularPointCoordinates.RegularBilinearData.meanAt_toContinuousLinearMap line 32
  3. theorem OAI.RegularPointCoordinates.RegularBilinearData.meanAt_isPositive line 40
  4. def OAI.RegularPointCoordinates.RegularBilinearData.pinchingMassMatrix line 46

    Source documentation

    These matrices retain the full original Bochner measure and use the mean at a fixed dyadic offset. Their mass radius is one third of that mean radius.

    def pinchingMassMatrix (i : ℕ) : Euclidean n →L[ℝ] Euclidean n :=
…

    Mentions: OAI.RegularPointCoordinates.Euclidean

  5. theorem OAI.RegularPointCoordinates.RegularBilinearData.pinchingMassMatrix_isPositive line 51
  6. theorem OAI.RegularPointCoordinates.regular_pinching_matrix_identification line 63

    Source documentation

    The matrix furnished by the pinching proof equals the canonical mean matrix at the shifted dyadic index. This identification uses equality of operators, without comparing or commuting arbitrary normalization frames.

    theorem regular_pinching_matrix_identification {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} [(hausdorff n X).Regular]
    {base : X} {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker} {enlargement zeta : ℝ}
    (d : RegularBilinearData hX base hk enlargement zeta)
    (q : X) (hq : q ∈ ball base (d.radius / 32)) (i : ℕ)
    (R : Euclidean n ≃L[ℝ] Euclidean n)
    (hR : R.toContinuousLinearMap = sobolevMeanGram (hausdorff n X) hX.quadratic
      (sobolevColumnMap (hausdorff n X) hX.quadratic d.coordinates)
      (ball q (3 * (distanceSourceRadius d.radius i / 49152))) measurableSet_ball) :
    R = d.meanAt q hq (i + 15) := by
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularBilinearData, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.distanceSourceRadius