RegularPairCommutator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual commutator on the common radial-fit ball

theorem OAI.RegularPointCoordinates.centered_transformed_columnMap line 19
Source documentation
The centered finite column and the centered linear family are exactly the same Sobolev map, before any local representatives are chosen.
```
theorem centered_transformed_columnMap (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (eta : SobolevSpace μ hQ) (z : Euclidean n) :
    sobolevColumnMap μ hQ (centeredColumn μ hQ (transformedColumn μ hQ u N)
      ((N : Euclidean n →L[ℝ] Euclidean n).adjoint z) eta) =
      (centeredSobolevMap μ hQ u eta z).comp N.toContinuousLinearMap := by
…
```
Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.centeredColumn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.centeredSobolevMap

theorem OAI.RegularPointCoordinates.regular_pair_commutator line 36

Source documentation

The published commutator bound applies to any chosen radial families on the common small ball. The sole loss is its explicit volume ratio.

theorem regular_pair_commutator {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (haction : LocalPoissonHessianActionInput hX)
    {base first center : X} {a κ B J C A Cχ enlargement zeta eta Cg D Ca : ℝ}
    {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
    (hcenter : center ∈ ball base (e.heat.radius / 32))
    (d1 : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca first)
    (d2 : RegularCenterRadialData hX e.heat κ B J C A Cχ eta Cg D Ca center)
    (hκ : 0 ≤ κ) (hK : -κ ≤ K) (hB : 0 ≤ B) (hJ : 0 ≤ J)
    (hA : 0 ≤ A) (hCχ : 0 ≤ Cχ) (hzeta : 0 ≤ zeta) (hzeta1 : zeta ≤ 1) (i : ℕ) :
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalPoissonHessianActionInput, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment, OAI.RegularPointCoordinates.RegularCenterRadialData