FixedMinimumEstimates.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.FixedMinimum.relativeValue line 15
Source documentation
The affine value relative to the constant-slope branch t.
```
def relativeValue {ι : Type uIota} [Fintype ι]
    (t : ℝ) (r p : ι → ℝ) (h c : ℝ) : ℝ :=
…
```

theorem OAI.Problem326.FixedMinimum.tendsto_rpow_ratio line 21

Source documentation

A strict limiting exponent gap makes the normalized monomial vanish. This formulation permits the approximating exponents to leave their cube.

theorem tendsto_rpow_ratio {h p : ℕ → ℝ} {q p₀ : ℝ}
    (hh : ∀ n, 0 < h n) (hh0 : Tendsto h atTop (𝓝 0))
    (hp : Tendsto p atTop (𝓝 p₀)) (hqp : q < p₀) :
    Tendsto (fun n => h n ^ p n / h n ^ q) atTop (𝓝 0) := by
…

theorem OAI.Problem326.FixedMinimum.tendsto_normalized_sum line 33

Source documentation

Finite sums of monomials whose nonzero coefficients have exponent above q are negligible relative to h^q.

theorem tendsto_normalized_sum {ι : Type uIota} [Fintype ι]
    {h : ℕ → ℝ} {p : ℕ → ι → ℝ} {p₀ a : ι → ℝ} {q : ℝ}
    (hh : ∀ n, 0 < h n) (hh0 : Tendsto h atTop (𝓝 0))
    (hp : ∀ i, Tendsto (fun n => p n i) atTop (𝓝 (p₀ i)))
    (hgap : ∀ i, a i ≠ 0 → q < p₀ i) :
    Tendsto (fun n => (∑ i, a i * h n ^ p n i) / h n ^ q)
      atTop (𝓝 0) := by
…

theorem OAI.Problem326.FixedMinimum.coefficient_nonpos_of_domination line 51

Source documentation

A positive coefficient in a nonnegative sum cannot be dominated by a strictly higher exponent, even in the presence of a negligible offset.

theorem coefficient_nonpos_of_domination
    {A B d : ℕ → ℝ} {c : ℝ}
    (hA : ∀ n, 0 < A n) (hB : ∀ n, 0 < B n)
    (hBA : Tendsto (fun n => B n / A n) atTop (𝓝 0))
    (hd : Tendsto (fun n => d n / B n) atTop (𝓝 0))
    (hdom : ∀ n, c * A n ≤ B n - d n) : c ≤ 0 := by
…

theorem OAI.Problem326.FixedMinimum.tendsto_rpow_ratio_of_gap line 67

Source documentation

The quotient version also allows a moving denominator exponent.

theorem tendsto_rpow_ratio_of_gap {h p q : ℕ → ℝ} {p₀ q₀ : ℝ}
    (hh : ∀ n, 0 < h n) (hh0 : Tendsto h atTop (𝓝 0))
    (hp : Tendsto p atTop (𝓝 p₀)) (hq : Tendsto q atTop (𝓝 q₀))
    (hqp : q₀ < p₀) :
    Tendsto (fun n => h n ^ p n / h n ^ q n) atTop (𝓝 0) := by
…

theorem OAI.Problem326.FixedMinimum.active_raised_exponent_ge line 80

Source documentation

Nonnegative raised coordinates of an active branch cannot have limiting exponent below the offset exponent.

theorem active_raised_exponent_ge {ι : Type uIota} [Fintype ι]
    {h c : ℕ → ℝ} {p : ℕ → ι → ℝ} {p₀ r : ι → ℝ} {t β : ℝ}
    (hh : ∀ n, 0 < h n) (hh0 : Tendsto h atTop (𝓝 0))
    (hp : ∀ i, Tendsto (fun n => p n i) atTop (𝓝 (p₀ i)))
    (hr : ∀ i, t ≤ r i)
    (hc : Tendsto (fun n => c n / h n ^ β) atTop (𝓝 (-1)))
    (hactive : ∀ n, relativeValue t r (p n) (h n) (c n) ≤ 0)
    {i : ι} (hi : t < r i) : β ≤ p₀ i := by
…

Mentions: OAI.Problem326.FixedMinimum.relativeValue

theorem OAI.Problem326.FixedMinimum.not_active_of_offset_gap line 115

Source documentation

A competitor with normalized value tending to -1 defeats any branch whose slope is coordinatewise above the baseline and whose normalized offset tends to zero. No continuity of either offset is needed.

theorem not_active_of_offset_gap {ι : Type uIota} [Fintype ι]
    {h c d : ℕ → ℝ} {p : ℕ → ι → ℝ} {p₀ r s : ι → ℝ} {t γ : ℝ}
    (hh : ∀ n, 0 < h n) (hh0 : Tendsto h atTop (𝓝 0))
    (hp : ∀ i, Tendsto (fun n => p n i) atTop (𝓝 (p₀ i)))
    (hr : ∀ i, t ≤ r i)
    (hc : Tendsto (fun n => c n / h n ^ γ) atTop (𝓝 0))
    (hd : Tendsto (fun n => d n / h n ^ γ) atTop (𝓝 (-1)))
    (hgap : ∀ i, s i ≠ t → γ < p₀ i) :
    ¬ (∀ n, relativeValue t r (p n) (h n) (c n) ≤
      relativeValue t s (p n) (h n) (d n)) := by
…

Mentions: OAI.Problem326.FixedMinimum.relativeValue

theorem OAI.Problem326.FixedMinimum.unraised_exponent_le line 147

Source documentation

The second exclusion in the fixed-minimum argument. A next-type competitor supported on U ∪ {j} forces every unraised exponent below its offset threshold.

theorem unraised_exponent_le {ι : Type uIota} [Fintype ι] [DecidableEq ι]
    {h c d : ℕ → ℝ} {p : ℕ → ι → ℝ} {p₀ r s : ι → ℝ}
    {t β γ : ℝ} {U : Finset ι} {j : ι}
    (hh : ∀ n, 0 < h n) (hh0 : Tendsto h atTop (𝓝 0))
    (hp : ∀ i, Tendsto (fun n => p n i) atTop (𝓝 (p₀ i)))
    (hr : ∀ i, t ≤ r i)
    (hc : Tendsto (fun n => c n / h n ^ γ) atTop (𝓝 0))
    (hd : Tendsto (fun n => d n / h n ^ γ) atTop (𝓝 (-1)))
    (hγβ : γ < β) (hpU : ∀ i ∈ U, β ≤ p₀ i)
    (hs : ∀ i, i ∉ U → i ≠ j → s i = t)
    (hactive : ∀ n, relativeValue t r (p n) (h n) (c n) ≤
      relativeValue t s (p n) (h n) (d n)) : p₀ j ≤ γ := by
…

Mentions: OAI.Problem326.FixedMinimum.relativeValue

theorem OAI.Problem326.FixedMinimum.last_unraised_eq_minimum line 172

Source documentation

When only one coordinate is unraised, the fixed minimum determines that coordinate exactly.

theorem last_unraised_eq_minimum {ι : Type uIota} {p : ι → ℝ} {t β : ℝ} {j : ι}
    (hmin : ∃ i, p i = t) (htβ : t < β)
    (hother : ∀ i, i ≠ j → β ≤ p i) : p j = t := by
…

theorem OAI.Problem326.FixedMinimum.error_of_raised_and_unraised line 185

Source documentation

Combining the inductive error on raised coordinates with the threshold bound on all other coordinates yields the full sup-norm error estimate.

theorem error_of_raised_and_unraised {ι : Type uIota} [Fintype ι]
    {p r : ι → ℝ} {U : Set ι} {t γ ε : ℝ}
    (hraised : ∀ i ∈ U, |p i - r i| < ε)
    (hr : ∀ i ∉ U, r i = t)
    (hlo : ∀ i ∉ U, t ≤ p i)
    (hhi : ∀ i ∉ U, p i ≤ γ) (hε : γ - t < ε) :
    ∀ i, |p i - r i| < ε := by
…

theorem OAI.Problem326.FixedMinimum.fixed_minimum_label_bound line 198