HarmonicBochnerConstruction.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Constructing the Bochner family of an actual first-order splitting map

def OAI.RegularPointCoordinates.splittingDirectionBound line 19
Source documentation
A uniform bound for all constant directions of the splitting map.
```
def splittingDirectionBound (n : ℕ) (ε : ℝ) (hε : 0 ≤ ε) : ℝ≥0 :=
…
```
theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.local_bochner line 24
Source documentation
Local calculus for the harmonic map gives a positive finite measure family satisfying the heat and mass identities.
```
theorem FirstOrderSplittingOn.local_bochner {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hpublished : LocalHarmonicBochnerInput hX)
    {κ : ℝ} (hκ : 0 ≤ κ) (hK : -κ ≤ K) {p : X} {r ε : ℝ}
    (hr : 0 < r) (hε : 0 ≤ ε)
    {u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic} {w : X → Euclidean n}
    (h : FirstOrderSplittingOn (hausdorff n X) hX.quadratic p (8 * r) ε u w) :
    ∃ M : PositiveBilinearMeasure X (Euclidean n),
      ∀ v, Nonempty (LocalHarmonicEnergy (hausdorff n X) hX.quadratic
        (sobolevColumnMap (hausdorff n X) hX.quadratic u) M κ p r
        (splittingDirectionBound n ε hε) v) := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicBochnerInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.splittingDirectionBound