DescentHolder.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.sum_le_card_rpow_mul_moment line 10

Source documentation

Finite Hölder with one factor equal to one, in the normalization used for the exceptional set in the descent.

theorem sum_le_card_rpow_mul_moment
    {ι : Type*} (H : Finset ι) (f : ι → ℝ) (r : ℝ)
    (hr : 1 < r) (hf : ∀ i ∈ H, 0 ≤ f i) :
    (∑ i ∈ H, f i) ≤
      (H.card : ℝ) ^ (1 - 1 / r) * (∑ i ∈ H, f i ^ r) ^ (1 / r) := by
…

theorem OAI.Problem337.normalized_moment_factor line 26

Source documentation

Algebraic normalization of the Hölder moment bound.

theorem normalized_moment_factor
    (x Y E r : ℝ) (hx : 0 ≤ x) (hY : 0 < Y) :
    x ^ (1 - 1 / r) * (Y * Real.exp E) ^ (1 / r) =
      Y * Real.exp (E / r) * (x / Y) ^ (1 - 1 / r) := by
…

theorem OAI.Problem337.descent_holder_bound line 42

Source documentation

A moment estimate on an ambient finite set controls its restriction to an exceptional set, including the empty exceptional set.

theorem descent_holder_bound
    {ι : Type*} (I H : Finset ι) (f : ι → ℝ) (Y E r : ℝ)
    (hHI : H ⊆ I) (hf : ∀ i ∈ I, 0 ≤ f i) (hY : 0 < Y) (hr : 1 < r)
    (hmoment : (∑ i ∈ I, f i ^ r) ≤ Y * Real.exp E) :
    (∑ i ∈ H, f i) ≤
      Y * Real.exp (E / r) * ((H.card : ℝ) / Y) ^ (1 - 1 / r) := by
…

theorem OAI.Problem337.indexed_descent_holder_bound line 68

Source documentation

Summing the uniform restricted moment estimate over a finite indexed family does not require that distinct indices have distinct values.

theorem indexed_descent_holder_bound
    {ι κ : Type*} (J : Finset ι) (I H : Finset κ) (f : ι → κ → ℝ)
    (Y E r : ℝ) (hHI : H ⊆ I) (hY : 0 < Y) (hr : 1 < r)
    (hf : ∀ j ∈ J, ∀ i ∈ I, 0 ≤ f j i)
    (hmoment : ∀ j ∈ J, (∑ i ∈ I, f j i ^ r) ≤ Y * Real.exp E) :
    (∑ j ∈ J, ∑ i ∈ H, f j i) ≤
      (J.card : ℝ) * (Y * Real.exp (E / r) *
        ((H.card : ℝ) / Y) ^ (1 - 1 / r)) := by
…

theorem OAI.Problem337.normalized_predecessor_bound line 86

Source documentation

Normalization of the indexed predecessor count. The factor 1 / ρ cancels because the next interval has length Y = ρ X.

theorem normalized_predecessor_bound
    (a B T X Y ρ ε E r J : ℝ) (hX : 0 < X) (hρ : 0 < ρ) (hJ : 0 < J)
    (hY : Y = ρ * X)
    (hpair : a ≤ X * ε + B + (2 / (ρ * J)) * T)
    (hsum : T ≤ J * (Y * Real.exp (E / r) * (B / Y) ^ (1 - 1 / r))) :
    a / X ≤ ε + ρ * (B / Y) + 2 * Real.exp (E / r) * (B / Y) ^ (1 - 1 / r) := by
…

theorem OAI.Problem337.absorb_inherited_proportion line 108

Source documentation

The inherited exceptional proportion can be absorbed into the same fractional power as the new predecessors.

theorem absorb_inherited_proportion
    (δ ε ρ E r : ℝ) (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
    (hρ1 : ρ ≤ 1) (hr : 1 < r) :
    ε + ρ * δ + 2 * Real.exp (E / r) * δ ^ (1 - 1 / r) ≤
      ε + (1 + 2 * Real.exp (E / r)) * δ ^ (1 - 1 / r) := by
…

theorem OAI.Problem337.descent_coefficient_bound line 121
Source documentation
A convenient exponential envelope for the coefficient in the normalized recurrence, once the moment parameter is at least two.
```
theorem descent_coefficient_bound
    (E r : ℝ) (hE : 2 ≤ E) (hr : 1 ≤ r) :
    1 + 2 * Real.exp (E / r) ≤ Real.exp (2 * E) := by
…
```

theorem OAI.Problem337.descent_recurrence_of_pair_and_moment line 137

Source documentation

The exact one-step recurrence used by the exceptional-density iteration. All moment and pair-count hypotheses remain explicit.

theorem descent_recurrence_of_pair_and_moment
    (a B T X Y ρ ε E r J : ℝ) (hX : 0 < X) (hρ : 0 < ρ)
    (hρ1 : ρ ≤ 1) (hJ : 0 < J) (hY : Y = ρ * X)
    (hB0 : 0 ≤ B) (hBY : B ≤ Y) (hE : 2 ≤ E) (hr : 1 < r)
    (hpair : a ≤ X * ε + B + (2 / (ρ * J)) * T)
    (hsum : T ≤ J * (Y * Real.exp (E / r) * (B / Y) ^ (1 - 1 / r))) :
    a / X ≤ ε + Real.exp (2 * E) * (B / Y) ^ (1 - 1 / r) := by
…