LargeValueSubsequence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A large-value subsequence is extracted from the actual finite moment.

lemma OAI.CubicFirstMoment.logarithmic_power_bounds line 12

theorem OAI.CubicFirstMoment.extract_large_value_subsequence line 28

Source documentation

Uniform elementary bounds and an unsaved moment yield actual selected rows and simultaneous logarithmic limits. Their exponents satisfy the large-value inequality, rather than having it as an assumption.

theorem extract_large_value_subsequence {ι κ : Type*} [Fintype ι] [DecidableEq ι]
    (Y G : ℕ → ℝ) (S : ℕ → Finset κ) (f : ℕ → ι → κ → ℝ)
    {H K D s : ℝ} (hH : 0 ≤ H) (hK : 0 ≤ K)
    (hY : Tendsto Y atTop atTop) (hY₁ : ∀ j, 1 < Y j)
    (hG : ∀ j, 0 < G j) (hGexp : HasPowerExponent Y G s)
    (hcard : ∀ j, ((S j).card:ℝ) ≤ (Y j)^D)
    (hlo : ∀ j, ∀ x ∈ S j, ∀ i, (Y j)^(-K) ≤ f j i x)
    (hhi : ∀ j, ∀ x ∈ S j, ∀ i, f j i x ≤ (Y j)^H)
    (hmoment : ∀ j, G j ≤ ∑ x ∈ S j, (∏ i, f j i x)^2) :
    ∃ (φ : ℕ → ℕ) (P : ℕ → Finset κ) (B : ℕ → ι → ℝ) (r : ℝ) (v : ι → ℝ),
      StrictMono φ ∧ (∀ j, (P j).Nonempty ∧ P j ⊆ S (φ j)) ∧
      (∀ j i, (Y (φ j))^(-K) ≤ B j i ∧ B j i ≤ (Y (φ j))^H) ∧
…

Mentions: OAI.CubicFirstMoment.HasPowerExponent