ScalarAbsorption.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.radial_energy_absorption line 11

Source documentation

The scalar absorption used after testing the radial transport equation.

theorem radial_energy_absorption {energy alpha error C : ℝ}
    (henergy : 0 ≤ energy)
    (hbound : energy ≤ C * (alpha ^ 2 + error ^ 2) +
      C * Real.sqrt energy * (alpha + error)) :
    energy ≤ 2 * (C + C ^ 2) * (alpha ^ 2 + error ^ 2) := by
…

theorem OAI.RegularPointCoordinates.contracting_recurrence_sq_sum line 23

Source documentation

A contractive recurrence has a uniform finite-scale square-sum estimate. The extra endpoint term makes the induction telescope without infinite sums.

theorem contracting_recurrence_sq_sum {b f : ℕ → ℝ} {C : ℝ}
    (hzero : b 0 = 0) (hpos : ∀ i, 0 ≤ b i)
    (hrec : ∀ i, b (i + 1) ≤ b i / 2 + C * f i) (k : ℕ) :
    (∑ i ∈ Finset.range k, b i ^ 2) + 2 * b k ^ 2 ≤
      4 * C ^ 2 * ∑ i ∈ Finset.range k, f i ^ 2 := by
…

theorem OAI.RegularPointCoordinates.contracting_recurrence_sq_sum_le line 39

Source documentation

The diagonal error estimate used when summing metric increments.

theorem contracting_recurrence_sq_sum_le {b f : ℕ → ℝ} {C : ℝ}
    (hzero : b 0 = 0) (hpos : ∀ i, 0 ≤ b i)
    (hrec : ∀ i, b (i + 1) ≤ b i / 2 + C * f i) (k : ℕ) :
    (∑ i ∈ Finset.range k, b i ^ 2) ≤
      4 * C ^ 2 * ∑ i ∈ Finset.range k, f i ^ 2 := by
…

theorem OAI.RegularPointCoordinates.contracting_recurrence_sq_sum_upto line 48

Source documentation

The same estimate needs the recurrence only below the scale being tested.

theorem contracting_recurrence_sq_sum_upto {b f : ℕ → ℝ} {C : ℝ}
    (k : ℕ) (hzero : b 0 = 0) (hpos : ∀ i, 0 ≤ b i)
    (hrec : ∀ i < k, b (i + 1) ≤ b i / 2 + C * f i) :
    (∑ i ∈ Finset.range k, b i ^ 2) + 2 * b k ^ 2 ≤
      4 * C ^ 2 * ∑ i ∈ Finset.range k, f i ^ 2 := by
…