MeanGramControl.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

From averaged splitting-map errors to exact Gram normalization

theorem OAI.RegularPointCoordinates.abs_average_sub_const_le line 19

Source documentation

The normalized integral of the absolute error controls the error of its mean on a positive finite-measure set.

theorem abs_average_sub_const_le (s : Set X)
    (hzero : μ s ≠ 0) (hfin : μ s ≠ ∞) {f : X → ℝ}
    (hf : IntegrableOn f s μ) (c : ℝ) :
    |(μ.real s)⁻¹ * (∫ x in s, f x ∂μ) - c| ≤
      (μ.real s)⁻¹ * ∫ x in s, |f x - c| ∂μ := by
…

theorem OAI.RegularPointCoordinates.meanGram_sub_id_norm_le line 41

Source documentation

The first-order averaged Gram errors in a splitting-map definition bound the actual mean Gram operator in Euclidean operator norm.

theorem meanGram_sub_id_norm_le {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (s : Set X) (hs : MeasurableSet s) (hzero : μ s ≠ 0) (hfin : μ s ≠ ∞)
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (herror : ∀ i j : Fin n,
      (μ.real s)⁻¹ * ∫ x in s,
        |localGamma μ hQ (u i) (u j) x - (if i = j then 1 else 0)| ∂μ ≤ epsilon) :
    ‖sobolevMeanGram μ hQ (sobolevColumnMap μ hQ u) s hs -
      ContinuousLinearMap.id ℝ (Euclidean n)‖ ≤ (n : ℝ) ^ 2 * epsilon := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.inner_lower_of_sub_id_norm line 64

Source documentation

Small operator error yields the quantitative lower bound for the quadratic form without assuming that the Gram operator is invertible.

theorem inner_lower_of_sub_id_norm {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] (Q : E →L[ℝ] E) {delta : ℝ}
    (hbound : ‖Q - ContinuousLinearMap.id ℝ E‖ ≤ delta) (v : E) :
    (1 - delta) * ‖v‖ ^ 2 ≤ ⟪v, Q v⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.inner_upper_of_sub_id_norm line 78

Source documentation

The matching upper quadratic-form bound.

theorem inner_upper_of_sub_id_norm {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] (Q : E →L[ℝ] E) {delta : ℝ}
    (hbound : ‖Q - ContinuousLinearMap.id ℝ E‖ ≤ delta) (v : E) :
    ⟪v, Q v⟫_ℝ ≤ (1 + delta) * ‖v‖ ^ 2 := by
…

theorem OAI.RegularPointCoordinates.exact_mean_normalizer_bounds line 93

Source documentation

First-order Gram error bounds control both an exact normalizer and its inverse. No closeness or norm bound for the chosen normalizer is assumed.

theorem exact_mean_normalizer_bounds {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (s : Set X) (hs : MeasurableSet s) (hzero : μ s ≠ 0) (hfin : μ s ≠ ∞)
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (herror : ∀ i j : Fin n,
      (μ.real s)⁻¹ * ∫ x in s,
        |localGamma μ hQ (u i) (u j) x - (if i = j then 1 else 0)| ∂μ ≤ epsilon)
    (A : Euclidean n ≃L[ℝ] Euclidean n)
    (hA : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u) s hs A)
    (v : Euclidean n) :
    (1 - (n : ℝ) ^ 2 * epsilon) * ‖A v‖ ^ 2 ≤ ‖v‖ ^ 2 ∧
      ‖A.symm v‖ ^ 2 ≤ (1 + (n : ℝ) ^ 2 * epsilon) * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.exists_exact_mean_normalization_of_gram_error line 115

Source documentation

The averaged first-order splitting-map estimate alone constructs an exact mean normalizer once the dimension-dependent error is less than one.

theorem exists_exact_mean_normalization_of_gram_error {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (s : Set X) (hs : MeasurableSet s)
    (hzero : μ s ≠ 0) (hfin : μ s ≠ ∞) {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (hsmall : (n : ℝ) ^ 2 * epsilon < 1)
    (herror : ∀ i j : Fin n,
      (μ.real s)⁻¹ * ∫ x in s,
        |localGamma μ hQ (u i) (u j) x - (if i = j then 1 else 0)| ∂μ ≤ epsilon) :
    ∃ A : Euclidean n ≃L[ℝ] Euclidean n,
      IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u) s hs A := by
…