TruncatedLargeValues.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removing tiny factors before extracting the actual large-value rows.

theorem OAI.CubicFirstMoment.HasPowerExponent.variable_rpow line 14
Source documentation
Variable powers have exactly the exponent approached by their powers. This includes the lower sequences arising from successively smaller saving losses.
```
theorem HasPowerExponent.variable_rpow {Y a : ℕ → ℝ} {s : ℝ}
    (hY : Tendsto Y atTop atTop) (ha : Tendsto a atTop (𝓝 s)) :
    HasPowerExponent Y (fun j => (Y j)^(a j)) s := by
…
```
Mentions: OAI.CubicFirstMoment.HasPowerExponent
lemma OAI.CubicFirstMoment.small_factor_power_identity line 21

theorem OAI.CubicFirstMoment.retain_large_factor_moment line 31

Source documentation

The full finite moment retains at least half its lower bound after removing every row with a tiny factor. The exponent of the cutoff is fixed.

theorem retain_large_factor_moment {ι κ : Type*} [Fintype ι] [DecidableEq ι]
    (S : Finset κ) (f : ι → κ → ℝ) {Y G D H K : ℝ}
    (hY : 2 ≤ Y) (hG : 1 ≤ G) (hH : 0 ≤ H)
    (hK : D+2*(Fintype.card ι:ℝ)*H-2*K ≤ -2)
    (hcard : (S.card:ℝ) ≤ Y^D)
    (hf : ∀ x ∈ S, ∀ i, 0 ≤ f i x)
    (hhi : ∀ x ∈ S, ∀ i, f i x ≤ Y^H)
    (hmoment : G ≤ ∑ x ∈ S, (∏ i, f i x)^2) :
    G/2 ≤ ∑ x ∈ S with ∀ i, Y^(-K) ≤ f i x, (∏ i, f i x)^2 := by
…

theorem OAI.CubicFirstMoment.extract_unsaved_moment_subsequence line 57

Source documentation

An unsaved actual moment with boundedly many polynomially bounded factor amplitudes produces genuine large-value rows and their limiting exponents. Zero and arbitrarily tiny values are allowed in the input.

theorem extract_unsaved_moment_subsequence {ι κ : Type*} [Fintype ι] [DecidableEq ι]
    (Y G : ℕ → ℝ) (S : ℕ → Finset κ) (f : ℕ → ι → κ → ℝ)
    {H K D s : ℝ} (hH : 0 ≤ H) (hK : 0 ≤ K)
    (hcut : D+2*(Fintype.card ι:ℝ)*H-2*K ≤ -2)
    (hY : Tendsto Y atTop atTop) (hY₂ : ∀ j, 2 ≤ Y j)
    (hG : ∀ j, 1 ≤ G j) (hGexp : HasPowerExponent Y G s)
    (hcard : ∀ j, ((S j).card:ℝ) ≤ (Y j)^D)
    (hf : ∀ j, ∀ x ∈ S j, ∀ i, 0 ≤ 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)) ∧
…

Mentions: OAI.CubicFirstMoment.HasPowerExponent