AffineGluing.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.AffineGluing.eventually_pos_sum_add_scale line 15

Source documentation

A positive comparison scale dominates a finite affine error that is little-o of it.

theorem eventually_pos_sum_add_scale {α : Type uAlpha} {ι : Type uIota} [Fintype ι]
    {l : Filter α} {x : ι → α → ℝ} {c s : α → ℝ} (a : ι → ℝ)
    (hs : ∀ᶠ n in l, 0 < s n) (hc : c =o[l] s)
    (hx : ∀ i, x i =o[l] s) :
    ∀ᶠ n in l, 0 < (∑ i, a i * x i n) + c n + s n := by
…

theorem OAI.Problem326.AffineGluing.eventually_pos_sum_add_sub_scale line 32

Source documentation

One positive coordinate contribution that dominates the comparison scale also dominates all nonnegative remaining contributions and a little-o offset.

theorem eventually_pos_sum_add_sub_scale {α : Type uAlpha} {ι : Type uIota} [Fintype ι]
    {l : Filter α} {x : ι → α → ℝ} {c s : α → ℝ} (a : ι → ℝ) (j : ι)
    (ha : ∀ i, 0 ≤ a i) (haj : 0 < a j)
    (hs : ∀ᶠ n in l, 0 < s n) (hc : c =o[l] s)
    (hx : ∀ᶠ n in l, ∀ i, 0 ≤ x i n)
    (hj : Tendsto (fun n => x j n / s n) l atTop) :
    ∀ᶠ n in l, 0 < (∑ i, a i * x i n) + c n - s n := by
…

theorem OAI.Problem326.AffineGluing.active_upper_cut line 55

Source documentation

The upper comparison in affine gluing forces some limiting exponent below the cut. The asymptotic hypotheses are exactly the variable-exponent power estimates.

theorem active_upper_cut {ι : Type uIota} [Fintype ι]
    {x : ι → ℕ → ℝ} {c s : ℕ → ℝ} (a p : ι → ℝ) (q : ℝ)
    (hs : ∀ᶠ n in atTop, 0 < s n) (hc : c =o[atTop] s)
    (hgap : ∀ i, q < p i → x i =o[atTop] s)
    (hactive : ∀ᶠ n in atTop, (∑ i, a i * x i n) + c n + s n ≤ 0) :
    ∃ i, p i ≤ q := by
…

theorem OAI.Problem326.AffineGluing.active_lower_cut line 69

Source documentation

The lower comparison in affine gluing forces every limiting exponent above the cut.

theorem active_lower_cut {ι : Type uIota} [Fintype ι]
    {x : ι → ℕ → ℝ} {c s : ℕ → ℝ} (a p : ι → ℝ) (q : ℝ)
    (ha : ∀ i, 0 < a i)
    (hs : ∀ᶠ n in atTop, 0 < s n) (hc : c =o[atTop] s)
    (hx : ∀ᶠ n in atTop, ∀ i, 0 ≤ x i n)
    (hgap : ∀ i, p i < q → Tendsto (fun n => x i n / s n) atTop atTop)
    (hactive : ∀ᶠ n in atTop, (∑ i, a i * x i n) + c n - s n ≤ 0) :
    ∀ i, q ≤ p i := by
…

theorem OAI.Problem326.AffineGluing.active_upper_cut_on_support line 86

Source documentation

A supported version of the upper comparison: coordinates with zero coefficient need no asymptotic control. This is useful in the fixed-minimum induction.

theorem active_upper_cut_on_support {ι : Type uIota} [Fintype ι]
    {x : ι → ℕ → ℝ} {c s : ℕ → ℝ} (a p : ι → ℝ) (q : ℝ)
    (hs : ∀ᶠ n in atTop, 0 < s n) (hc : c =o[atTop] s)
    (hgap : ∀ i, a i ≠ 0 → q < p i → x i =o[atTop] s)
    (hactive : ∀ᶠ n in atTop, (∑ i, a i * x i n) + c n + s n ≤ 0) :
    ∃ i, a i ≠ 0 ∧ p i ≤ q := by
…

theorem OAI.Problem326.AffineGluing.active_nonnegative_lower_cut line 113

Source documentation

With nonnegative contributions, only strictly positive coefficients force a lower bound on the corresponding limiting exponent.

theorem active_nonnegative_lower_cut {ι : Type uIota} [Fintype ι]
    {x : ι → ℕ → ℝ} {c s : ℕ → ℝ} (a p : ι → ℝ) (q : ℝ)
    (ha : ∀ i, 0 ≤ a i)
    (hs : ∀ᶠ n in atTop, 0 < s n) (hc : c =o[atTop] s)
    (hx : ∀ᶠ n in atTop, ∀ i, 0 ≤ x i n)
    (hgap : ∀ i, p i < q → Tendsto (fun n => x i n / s n) atTop atTop)
    (hactive : ∀ᶠ n in atTop, (∑ i, a i * x i n) + c n - s n ≤ 0) :
    ∀ i, 0 < a i → q ≤ p i := by
…

theorem OAI.Problem326.AffineGluing.common_shift_comparison line 129
Source documentation
Common offset shifts preserve all comparisons inside a local family.
```
theorem common_shift_comparison (a b shift : ℝ) :
    a - shift ≤ b - shift ↔ a ≤ b := sub_le_sub_iff_right shift
```
theorem OAI.Problem326.AffineGluing.shifted_active_upper_cut line 132
theorem OAI.Problem326.AffineGluing.shifted_active_lower_cut line 146