LocalBochnerTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Transport of the canonical Bochner family

One positive bilinear measure supplies every local coordinate normalization. Restriction and linear coordinate changes preserve this measure and its singular part through the corresponding pullbacks.

def OAI.RegularPointCoordinates.LocalHarmonicEnergy.restrict line 30
Source documentation
Restriction keeps the same energy representative and the same measure.
```
def LocalHarmonicEnergy.restrict
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    {q : X} {s : ℝ} (hsub : ball q (2 * s) ⊆ ball p (2 * r)) :
    LocalHarmonicEnergy μ hQ U M κ q s L v where
…
```
Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy
def OAI.RegularPointCoordinates.LocalHarmonicEnergy.comp line 42
Source documentation
Linear coordinate changes pull back the full positive measure, including its singular part. The global extension bound pays only the operator norm.
```
def LocalHarmonicEnergy.comp (A : E →L[ℝ] E)
    (G : LocalHarmonicEnergy μ hQ U M κ p r L (A v)) :
    LocalHarmonicEnergy μ hQ (U.comp A) (M.comap A.toLinearMap) κ p r (L * ‖A‖₊) v where
…
```
Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy

theorem OAI.RegularPointCoordinates.transformed_harmonic_mass_le line 59

Source documentation

A normalized splitting error controls the original Bochner measure in the transformed direction. All scales use the same original measure.

theorem transformed_harmonic_mass_le [IsFiniteMeasureOnCompacts μ]
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X (Euclidean n))
    {p : X} {r ρ C κ : ℝ} {L : ℝ≥0}
    (G : ∀ v, LocalHarmonicEnergy μ hQ (sobolevColumnMap μ hQ u) M κ p r L v)
    (A : Euclidean n ≃L[ℝ] Euclidean n)
    (χ : GoodLaplacianCutoff μ hQ p ρ C)
    (hρ : 0 < ρ) (hρr : ρ < r) (hC : 0 ≤ C) (hκ : 0 ≤ κ)
    {ε : ℝ} (hε : 0 ≤ ε)
    (herror : ∀ i j : Fin n, ∫ x in closedBall p (2 * ρ),
      |localGamma μ hQ (transformedColumn μ hQ u A i)
        (transformedColumn μ hQ u A j) x - (if i = j then 1 else 0)| ∂μ ≤ ε)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.transformedColumn

theorem OAI.RegularPointCoordinates.transformed_normalized_bochner_mass_le line 92

Source documentation

The dimensionless splitting estimate applies to the same original measure in every transformed direction.

theorem transformed_normalized_bochner_mass_le [IsFiniteMeasureOnCompacts μ]
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X (Euclidean n))
    {p : X} {r ε C κ : ℝ} {L : ℝ≥0}
    (G : ∀ v, LocalHarmonicEnergy μ hQ (sobolevColumnMap μ hQ u) M κ p r L v)
    (A : Euclidean n ≃L[ℝ] Euclidean n) {w : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ p (8 * r) ε (transformedColumn μ hQ u A) w)
    (hr : 0 < r) (hε : 0 ≤ ε) (hC : 0 ≤ C) (hκ : 0 ≤ κ)
    (hvol : 0 < μ.real (ball p (8 * r)))
    (χ : GoodLaplacianCutoff μ hQ p (r / 2) C) (v : Euclidean n) :
    (r ^ 2 / μ.real (ball p (8 * r))) * ⟪A v, M.massOperator (ball p (r / 2)) (A v)⟫_ℝ ≤
      (2 * C * (n : ℝ) ^ 2 * ε + κ * r ^ 2 * ((n : ℝ) ^ 2 * ε + 1)) * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.GoodLaplacianCutoff

theorem OAI.RegularPointCoordinates.original_gram_bochner_mass_le line 121

Source documentation

Returning from exact normalized directions gives a relative mass bound in the original mean Gram.

theorem original_gram_bochner_mass_le [IsFiniteMeasureOnCompacts μ]
    {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X (Euclidean n))
    {p : X} {r ε C κ : ℝ} {L : ℝ≥0}
    (G : ∀ v, LocalHarmonicEnergy μ hQ (sobolevColumnMap μ hQ u) M κ p r L v)
    (A : Euclidean n ≃L[ℝ] Euclidean n) {w : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ p (8 * r) ε (transformedColumn μ hQ u A) w)
    (hexact : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
      (ball p (8 * r)) measurableSet_ball A)
    (hr : 0 < r) (hε : 0 ≤ ε) (hC : 0 ≤ C) (hκ : 0 ≤ κ)
    (hvol : 0 < μ.real (ball p (8 * r)))
    (χ : GoodLaplacianCutoff μ hQ p (r / 2) C) (v : Euclidean n) :
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.GoodLaplacianCutoff