OAI/Geometry/RCD/Coordinates/NormalizationCumulative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.inverse_normalization_errors_sum_le line 17

   Source documentation

   Summing the proved inverse-normalization estimate over at most J centers per scale preserves its weighted heat total.

   theorem inverse_normalization_errors_sum_le
       (Q : ℕ → E ≃L[ℝ] E) (R : ℕ → ι → E ≃L[ℝ] E)
       (F : ℕ → E →L[ℝ] E) (s : ℕ → Finset ι)
       (hQ : ∀ i, (Q i : E →L[ℝ] E).IsPositive)
       (hR : ∀ i y, y ∈ s i → (R i y : E →L[ℝ] E).IsPositive)
       (hF : ∀ i, (F i).IsPositive) {c C : ℝ} (hc : 0 < c) (hC : 0 ≤ C)
       (hcompare : ∀ i y, y ∈ s i → ∀ v, c * ⟪v, Q i v⟫_ℝ ≤ ⟪v, R i y v⟫_ℝ)
       (hbilinear : ∀ i y, y ∈ s i → ∀ u v,
         ⟪v, ((R i y : E →L[ℝ] E) - (Q i : E →L[ℝ] E)) u⟫_ℝ ^ 2 ≤
           (C * ⟪u, F i u⟫_ℝ) * ⟪v, Q i v⟫_ℝ)
       (J : ℕ) (hcard : ∀ i, (s i).card ≤ J) (xi : E) (k : ℕ) :
       (∑ i ∈ Finset.range k, ∑ y ∈ s i,
   …

2. theorem OAI.RegularPointCoordinates.normalization_mass_errors_sum_le line 54

   Source documentation

   A small positive mass form charges a normalization error by at most epsilon times its energy in the reference metric.

   theorem normalization_mass_errors_sum_le
       (Q : ℕ → E →L[ℝ] E) (C : ℕ → ι → E →L[ℝ] E)
       (s : ℕ → Finset ι) (e : ℕ → ι → E) {epsilon : ℝ}
       (hsmall : ∀ i y, y ∈ s i → ∀ v, ⟪v, C i y v⟫_ℝ ≤ epsilon * ⟪v, Q i v⟫_ℝ)
       (k : ℕ) :
       (∑ i ∈ Finset.range k, ∑ y ∈ s i, ⟪e i y, C i y (e i y)⟫_ℝ) ≤
         epsilon * ∑ i ∈ Finset.range k, ∑ y ∈ s i, ⟪e i y, Q i (e i y)⟫_ℝ := by
   …

3. theorem OAI.RegularPointCoordinates.inverse_normalized_mass_le line 67

   Source documentation

   Changing inverse normalization preserves the small pointwise mass bound.

   theorem inverse_normalized_mass_le (Q R : E ≃L[ℝ] E)
       (hQ : (Q : E →L[ℝ] E).IsPositive) (hR : (R : E →L[ℝ] E).IsPositive)
       (D : E →L[ℝ] E) {c epsilon : ℝ} (hc : 0 < c) (hepsilon : 0 ≤ epsilon)
       (hcompare : ∀ v, c * ⟪v, Q v⟫_ℝ ≤ ⟪v, R v⟫_ℝ)
       (hsmall : ∀ v, ⟪v, D v⟫_ℝ ≤ epsilon * ⟪v, Q v⟫_ℝ) (xi : E) :
       ⟪R.symm xi, D (R.symm xi)⟫_ℝ ≤ epsilon / c ^ 2 * ⟪xi, Q.symm xi⟫_ℝ := by
   …

4. theorem OAI.RegularPointCoordinates.local_mass_cumulative_comparison line 83

   Source documentation

   The finite-family part of the cumulative comparison. Its inputs are weighted totals and the central estimate proved from the heat decrements; all changes of normalization and the reverse covering argument are proved here. The vectors z i y may be the actual local inverse images.

   theorem local_mass_cumulative_comparison
       (N : ℕ → E →L[ℝ] E) (C : ℕ → ι → E →L[ℝ] E)
       (s : ℕ → Finset ι) (theta : ℕ → ι → ℝ)
       (a : ℕ → E) (z : ℕ → ι → E)
       (hC : ∀ i y, y ∈ s i → (C i y).IsPositive)
       (htheta : ∀ i y, y ∈ s i → 0 ≤ theta i y)
       (hcover : ∀ i, ∃ y ∈ s i, theta i y = 1 ∧
         ∀ v, ⟪v, N i v⟫_ℝ ≤ ⟪v, C i y v⟫_ℝ)
       {H t U V K epsilon : ℝ} (hH : 0 ≤ H) (hK : 0 ≤ K) (k : ℕ)
       (hupper : (∑ i ∈ Finset.range k, ∑ y ∈ s i, ⟪a i, C i y (a i)⟫_ℝ) ≤ U * H)
       (herror : (∑ i ∈ Finset.range k, ∑ y ∈ s i,
         ⟪z i y - a i, C i y (z i y - a i)⟫_ℝ) ≤ V * epsilon * H)
   …