LargeValueExtraction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite logarithmic pigeonholing and compact extraction of large rows.

lemma OAI.CubicFirstMoment.logarithmic_bucket line 14

Source documentation

Unit-width logarithmic bins have an absolute multiplicative width.

lemma logarithmic_bucket {τ x : ℝ} (hτ : 0 < τ) (hx : τ ≤ x) :
    τ*Real.exp (⌊Real.log (x/τ)⌋₊:ℝ) ≤ x ∧
      x ≤ Real.exp 1*(τ*Real.exp (⌊Real.log (x/τ)⌋₊:ℝ)) := by
…

theorem OAI.CubicFirstMoment.finite_logarithmic_large_values line 34

Source documentation

An actual finite moment has a nonempty logarithmic box carrying at least its average energy. The loss is the explicit number of boxes.

theorem finite_logarithmic_large_values (S : Finset κ) (f : ι → κ → ℝ)
    {τ U : ℝ} (hτ : 0 < τ)
    (hlo : ∀ x ∈ S, ∀ i, τ ≤ f i x) (hhi : ∀ x ∈ S, ∀ i, f i x ≤ U)
    (hm : 0 < ∑ x ∈ S, (∏ i, f i x)^2) :
    ∃ (P : Finset κ) (B : ι → ℝ), P.Nonempty ∧ P ⊆ S ∧
      (∀ i, τ ≤ B i ∧ B i ≤ U) ∧
      (∀ x ∈ P, ∀ i, B i ≤ f i x ∧ f i x ≤ Real.exp 1*B i) ∧
      (∑ x ∈ S, (∏ i, f i x)^2) ≤
        ((⌊Real.log (U/τ)⌋₊+1:ℕ)^Fintype.card ι:ℝ)*
          (Real.exp 1)^(2*Fintype.card ι)*(P.card:ℝ)*(∏ i, B i)^2 := by
…

lemma OAI.CubicFirstMoment.product_le_small_factor line 113

theorem OAI.CubicFirstMoment.discard_small_factor_moment line 130

Source documentation

Rows with an extremely small factor have uniformly negligible total energy once all other factors have their elementary upper bound.

theorem discard_small_factor_moment (S : Finset κ) (f : ι → κ → ℝ)
    {τ U : ℝ} (hU : 1 ≤ U)
    (hf : ∀ x ∈ S, ∀ i, 0 ≤ f i x)
    (hbound : ∀ x ∈ S, ∀ i, f i x ≤ U) :
    (∑ x ∈ S, (∏ i, f i x)^2) ≤
      (∑ x ∈ S with ∀ i, τ ≤ f i x, (∏ i, f i x)^2)+
        (S.card:ℝ)*(τ*U^(Fintype.card ι))^2 := by
…

theorem OAI.CubicFirstMoment.bounded_logarithms_subsequence line 159

Source documentation

Compactness supplies simultaneous limiting exponents of the actual selected row counts and factor scales.

theorem bounded_logarithms_subsequence {δ : Type*} [Finite δ]
    (Y : ℕ → ℝ) (f : δ → ℕ → ℝ) (l u : δ → ℝ)
    (hbound : ∀ j i, l i ≤ Real.log (f i j)/Real.log (Y j) ∧
      Real.log (f i j)/Real.log (Y j) ≤ u i) :
    ∃ (a : δ → ℝ) (φ : ℕ → ℕ), StrictMono φ ∧
      (∀ i, l i ≤ a i ∧ a i ≤ u i) ∧
      ∀ i, HasPowerExponent (Y ∘ φ) (f i ∘ φ) (a i) := by
…

Mentions: OAI.CubicFirstMoment.HasPowerExponent