DyadicMeanControl.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Dyadic growth and relative error of actual mean Grams

Adjacent relative estimates give an explicit outward growth bound and an error that is linear in the original splitting error. This is the bound needed when summing Gaussian annuli in a frame normalized at a small radius.

theorem OAI.RegularPointCoordinates.relative_sequence_growth line 23

Source documentation

Adjacent relative bounds propagate outwards, retaining a factor of the small error in the difference from the initial value.

theorem relative_sequence_growth {s : ℕ → ℝ} {δ : ℝ}
    (hδ : 0 ≤ δ) (hδhalf : δ ≤ 1 / 2) (k : ℕ)
    (hs : ∀ j ≤ k, 0 ≤ s j)
    (hstep : ∀ j < k, (1 - δ) * s (j + 1) ≤ s j ∧ s j ≤ (1 + δ) * s (j + 1)) :
    s k ≤ 2 ^ k * s 0 ∧ |s k - s 0| ≤ 2 * δ * (2 ^ k - 1) * s 0 := by
…

theorem OAI.RegularPointCoordinates.symmetric_norm_le_of_quadratic line 58

Source documentation

A symmetric operator norm is controlled by all of its quadratic forms, with no extra dimension factor.

theorem symmetric_norm_le_of_quadratic (A : E →L[ℝ] E) (hA : A.IsSymmetric)
    {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ v, |⟪v, A v⟫_ℝ| ≤ C * ‖v‖ ^ 2) :
    ‖A‖ ≤ C := by
…

theorem OAI.RegularPointCoordinates.normalized_mean_relative_norm_le line 75

Source documentation

A relative quadratic estimate for two actual means is an operator estimate in any exact normalizing frame for the reference mean.

theorem normalized_mean_relative_norm_le (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    [CompleteSpace E] (U : E →L[ℝ] SobolevSpace μ hQ)
    (s t : Set X) (hs : MeasurableSet s) (ht : MeasurableSet t)
    (A : E ≃L[ℝ] E) (hA : IsExactMeanNormalization μ hQ U s hs A)
    {C : ℝ} (hC : 0 ≤ C)
    (hrelative : ∀ v, |⟪v, sobolevMeanGram μ hQ U t ht v⟫_ℝ -
      ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ| ≤
        C * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ) :
    ‖sobolevMeanGram μ hQ (U.comp (A : E →L[ℝ] E)) t ht -
      ContinuousLinearMap.id ℝ E‖ ≤ C := by
…

Mentions: OAI.RegularPointCoordinates.QuadraticCheegerEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevMeanGram

theorem OAI.RegularPointCoordinates.dyadic_mean_growth line 102

Source documentation

Outward dyadic means of the same original harmonic map have linear relative error. Every adjacent premise comes from the proved normalization/Bishop--Gromov comparison.

theorem dyadic_mean_growth {K : ℝ} (m : ℕ) (hX : NoncollapsedRCD K (m + 1) X)
    {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
    (p : X) {r ε : ℝ} (hr : 0 < r) (hε : 0 ≤ ε)
    (hsmall : ((m + 1 : ℕ) : ℝ) ^ 2 * (normalizationVolumeRatio m * ε) ≤ 1 / 2)
    (k : ℕ) (hscale : ∀ j ≤ k, a * (3 * (2 ^ j * r)) ≤ 1)
    (hnormal : ∀ j ≤ k, ∃ (A : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
      (w : X → Euclidean (m + 1)),
      FirstOrderSplittingOn (hausdorff (m + 1) X) hX.quadratic p (2 ^ j * r) ε
        (transformedColumn (hausdorff (m + 1) X) hX.quadratic u A) w ∧
      IsExactMeanNormalization (hausdorff (m + 1) X) hX.quadratic
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizationVolumeRatio, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization