ScalarMetricBootstrap.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite-scale scalar metric bootstrap

Fixing a testing point and a direction turns the manuscript's matrix estimates into real sequences. Here z is the local mass in that direction, d is the weighted defect, and b is the normalized diagonal second derivative. The signed first-order errors and nonnegative squared increment are kept explicit.

Finite summation and Cauchy--Schwarz estimates close the bootstrap from these scalar premises, without further geometric assumptions.

theorem OAI.RegularPointCoordinates.weighted_defect_sum_le line 26

Source documentation

Monotonicity of the scale metrics converts the unweighted defect budget to the weighted one used in the metric estimate.

theorem weighted_defect_sum_le {e H : ℕ → ℝ} {epsilon Q : ℝ}
    (he : ∀ i, 0 ≤ e i) (hQ : 0 ≤ Q) (k : ℕ)
    (hH : ∀ i < k, H i ≤ Q)
    (hebudget : (∑ i ∈ Finset.range k, e i) ≤ epsilon) :
    (∑ i ∈ Finset.range k, e i * H i) ≤ epsilon * Q := by
…

theorem OAI.RegularPointCoordinates.leading_metric_comparison line 41

Source documentation

The cumulative upper/lower local-mass comparisons imply the leading metric comparison before the signed error is introduced.

theorem leading_metric_comparison {s z : ℕ → ℝ} {base Q T : ℝ}
    (hbase : 0 ≤ base) (hT : 0 < T) (hs : ∀ i, 0 ≤ s i) (k : ℕ)
    (hsz : ∀ i < k, s i ≤ z i)
    (hlower : Q ≤ T * (base + ∑ i ∈ Finset.range k, s i))
    (hupper : base + (∑ i ∈ Finset.range k, z i) ≤ T * Q) :
    T⁻¹ * Q ≤ base + 2 * (∑ i ∈ Finset.range k, s i) ∧
      base + 2 * (∑ i ∈ Finset.range k, s i) ≤ 2 * T * Q := by
…

theorem OAI.RegularPointCoordinates.sum_sqrt_mul_sqrt_le line 57

Source documentation

Cauchy--Schwarz for square roots of nonnegative scalar budgets.

theorem sum_sqrt_mul_sqrt_le {z d : ℕ → ℝ}
    (hz : ∀ i, 0 ≤ z i) (hd : ∀ i, 0 ≤ d i) (k : ℕ) :
    (∑ i ∈ Finset.range k, Real.sqrt (z i) * Real.sqrt (d i)) ≤
      Real.sqrt (∑ i ∈ Finset.range k, z i) *
        Real.sqrt (∑ i ∈ Finset.range k, d i) := by
…

theorem OAI.RegularPointCoordinates.diagonal_recurrence_square_budget line 73

Source documentation

The diagonal recurrence converts the forcing budgets to a square sum.

theorem diagonal_recurrence_square_budget {z d b : ℕ → ℝ} {C : ℝ}
    (hz : ∀ i, 0 ≤ z i) (hd : ∀ i, 0 ≤ d i) (hb : ∀ i, 0 ≤ b i)
    (hbzero : b 0 = 0) (k : ℕ)
    (hrec : ∀ i < k, b (i + 1) ≤ b i / 2 +
      C * (Real.sqrt (z i) + Real.sqrt (d i))) :
    (∑ i ∈ Finset.range k, b i ^ 2) ≤
      8 * C ^ 2 * ((∑ i ∈ Finset.range k, z i) +
        ∑ i ∈ Finset.range k, d i) := by
…

theorem OAI.RegularPointCoordinates.scalar_metric_cumulative_error line 98

Source documentation

Summing the exact metric increment and estimating its three errors. Only the displayed finite-scale premises are used.

theorem scalar_metric_cumulative_error {m s z d b linear inverse square : ℕ → ℝ}
    {C epsilon : ℝ} (hC : 0 ≤ C)
    (hz : ∀ i, 0 ≤ z i) (hd : ∀ i, 0 ≤ d i) (hb : ∀ i, 0 ≤ b i)
    (hbzero : b 0 = 0) (k : ℕ)
    (hrec : ∀ i < k, b (i + 1) ≤ b i / 2 +
      C * (Real.sqrt (z i) + Real.sqrt (d i)))
    (hlinear : ∀ i < k, |linear i| ≤ C * Real.sqrt (z i) * Real.sqrt (d i))
    (hinverse : ∀ i < k, |inverse i| ≤ C * b i * Real.sqrt (d i))
    (hsquare : ∀ i < k, |square i| ≤ C * epsilon * (z i + d i))
    (hstep : ∀ i < k, m (i + 1) - m i =
      2 * s i + 2 * linear i + 2 * inverse i + square i) :
    |m k - m 0 - 2 * ∑ i ∈ Finset.range k, s i| ≤
…

def OAI.RegularPointCoordinates.scalarMetricErrorCoefficient line 164
Source documentation
An explicit coefficient for the cumulative metric error after using the local-mass and weighted-defect budgets.
```
noncomputable def scalarMetricErrorCoefficient (C T epsilon : ℝ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.scalarMetricErrorCoefficient_tendsto_zero line 170
Source documentation
The coefficient can be made arbitrarily small after fixing C and T.
```
theorem scalarMetricErrorCoefficient_tendsto_zero (C T : ℝ) :
    Tendsto (scalarMetricErrorCoefficient C T) (𝓝 0) (𝓝 0) := by
…
```
Mentions: OAI.RegularPointCoordinates.scalarMetricErrorCoefficient

theorem OAI.RegularPointCoordinates.scalar_metric_error_of_budgets line 179

Source documentation

The full finite metric error is proportional to the final directional metric Q, even if that metric grows with the scale.

theorem scalar_metric_error_of_budgets {m s z d b linear inverse square : ℕ → ℝ}
    {C T epsilon Q : ℝ} (hC : 0 ≤ C) (hT : 0 ≤ T)
    (hepsilon : 0 ≤ epsilon) (hQ : 0 ≤ Q)
    (hz : ∀ i, 0 ≤ z i) (hd : ∀ i, 0 ≤ d i) (hb : ∀ i, 0 ≤ b i)
    (hbzero : b 0 = 0) (k : ℕ)
    (hrec : ∀ i < k, b (i + 1) ≤ b i / 2 +
      C * (Real.sqrt (z i) + Real.sqrt (d i)))
    (hlinear : ∀ i < k, |linear i| ≤ C * Real.sqrt (z i) * Real.sqrt (d i))
    (hinverse : ∀ i < k, |inverse i| ≤ C * b i * Real.sqrt (d i))
    (hsquare : ∀ i < k, |square i| ≤ C * epsilon * (z i + d i))
    (hstep : ∀ i < k, m (i + 1) - m i =
      2 * s i + 2 * linear i + 2 * inverse i + square i)
…

theorem OAI.RegularPointCoordinates.scalar_metric_comparison_closes line 229

Source documentation

Leading metric comparison and a small cumulative error close the bootstrap.

theorem scalar_metric_comparison_closes {M leading Q T eta : ℝ}
    (hQ : 0 ≤ Q) (hT : 0 < T)
    (hlower : T⁻¹ * Q ≤ leading) (hupper : leading ≤ 2 * T * Q)
    (herror : |M - leading| ≤ eta * Q) (hsmall : eta ≤ (2 * T)⁻¹) :
    (2 * T)⁻¹ * Q ≤ M ∧ M ≤ (2 * T + (2 * T)⁻¹) * Q := by
…

theorem OAI.RegularPointCoordinates.scalar_metric_fourfold_comparison line 245

Source documentation

Choosing the bootstrap constant 4T gives its lower and upper bounds.

theorem scalar_metric_fourfold_comparison {M leading Q T eta : ℝ}
    (hQ : 0 ≤ Q) (hT : 1 ≤ T)
    (hlower : T⁻¹ * Q ≤ leading) (hupper : leading ≤ 2 * T * Q)
    (herror : |M - leading| ≤ eta * Q) (hsmall : eta ≤ (2 * T)⁻¹) :
    (4 * T)⁻¹ * Q ≤ M ∧ M ≤ (4 * T) * Q := by
…

theorem OAI.RegularPointCoordinates.scalar_metric_bootstrap line 263

Source documentation

The scalar recurrence, three error estimates, two budgets, and leading comparison imply the metric bootstrap bounds.

theorem scalar_metric_bootstrap {m s z d b linear inverse square : ℕ → ℝ}
    {C T epsilon Q : ℝ} (hC : 0 ≤ C) (hT : 1 ≤ T)
    (hepsilon : 0 ≤ epsilon) (hQ : 0 ≤ Q)
    (hz : ∀ i, 0 ≤ z i) (hd : ∀ i, 0 ≤ d i) (hb : ∀ i, 0 ≤ b i)
    (hbzero : b 0 = 0) (k : ℕ)
    (hrec : ∀ i < k, b (i + 1) ≤ b i / 2 +
      C * (Real.sqrt (z i) + Real.sqrt (d i)))
    (hlinear : ∀ i < k, |linear i| ≤ C * Real.sqrt (z i) * Real.sqrt (d i))
    (hinverse : ∀ i < k, |inverse i| ≤ C * b i * Real.sqrt (d i))
    (hsquare : ∀ i < k, |square i| ≤ C * epsilon * (z i + d i))
    (hstep : ∀ i < k, m (i + 1) - m i =
      2 * s i + 2 * linear i + 2 * inverse i + square i)
…