UniformOffsetDecay.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem326.power_isLittleO_at_zero line 12

theorem OAI.Problem326.exists_common_offset_decay line 28

Source documentation

Finitely many offsets with power decay strictly stronger than h^t share one stronger decay exponent. The individual powers may vary with the label.

theorem exists_common_offset_decay {ι : Type uIota} [Fintype ι] [Nonempty ι]
    (c : ι → ℝ → ℝ) (t : ℝ)
    (hc : ∀ i, ∃ β : ℝ, t < β ∧ c i =O[𝓝[>] 0] (fun h => h ^ β)) :
    ∃ η : ℝ, t < η ∧ ∀ i, c i =o[𝓝[>] 0] (fun h => h ^ η) := by
…

theorem OAI.Problem326.exists_radius_with_offset_decay line 45

Source documentation

A pre-existing localization radius can be shrunk so that all local offsets are little-o of h^(t+ρ), as required by the affine-family gluing argument.

theorem exists_radius_with_offset_decay {ι : Type uIota} [Fintype ι] [Nonempty ι]
    (c : ι → ℝ → ℝ) (t ρ₀ : ℝ) (hρ₀ : 0 < ρ₀)
    (hc : ∀ i, ∃ β : ℝ, t < β ∧ c i =O[𝓝[>] 0] (fun h => h ^ β)) :
    ∃ ρ : ℝ, 0 < ρ ∧ ρ < ρ₀ ∧
      ∀ i, c i =o[𝓝[>] 0] (fun h => h ^ (t + ρ)) := by
…

theorem OAI.Problem326.shifted_offset_isBigO line 63
Source documentation
The offsets produced by the type construction have the required big-O bound even though the leading negative power prevents a little-o bound at that same exponent.
```
theorem shifted_offset_isBigO {d : ℝ → ℝ} {β : ℝ}
    (hd : d =o[𝓝[>] 0] (fun h => h ^ β)) :
    (fun h => -(h ^ β) + d h) =O[𝓝[>] 0] (fun h => h ^ β) := by
…
```
theorem OAI.Problem326.shifted_offset_normalized_limit line 70
Source documentation
Normalizing a constructed negative-shift offset by its leading power gives limit -1; this is the exact sequential input used by fixed-minimum activity estimates.
```
theorem shifted_offset_normalized_limit {d : ℝ → ℝ} {β : ℝ}
    (hd : d =o[𝓝[>] 0] (fun h => h ^ β)) :
    Tendsto (fun h : ℝ => (-(h ^ β) + d h) / h ^ β)
      (𝓝[>] 0) (𝓝 (-1)) := by
…
```