Extremal.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Compact lexicographic extrema and quantitative second-moment estimates.

theorem OAI.DoublingHilbert.near_lexicographic_maximum line 12

Source documentation

Near a compact lexicographic maximum, the second coordinate has a uniform upper bound.

theorem near_lexicographic_maximum
    {K : Set (ℝ × ℝ)} (hK : IsCompact K) {A B : ℝ}
    (hfirst : ∀ p ∈ K, p.1 ≤ A)
    (hsecond : ∀ p ∈ K, p.1 = A → p.2 ≤ B)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ p ∈ K, A - δ < p.1 → p.2 ≤ B + ε := by
…

theorem OAI.DoublingHilbert.exists_lexicographic_maximum line 43

Source documentation

A nonempty compact set has a lexicographic maximum.

theorem exists_lexicographic_maximum {K : Set (ℝ × ℝ)}
    (hK : IsCompact K) (hne : K.Nonempty) :
    ∃ A B : ℝ, (A, B) ∈ K ∧
      (∀ p ∈ K, p.1 ≤ A) ∧ (∀ p ∈ K, p.1 = A → p.2 ≤ B) := by
…

theorem OAI.DoublingHilbert.lexicographic_affine_barrier line 59

Source documentation

An affine barrier bounds the second coordinate in terms of the first-coordinate deficit.

theorem lexicographic_affine_barrier
    {K : Set (ℝ × ℝ)} (hK : IsCompact K) {A B M : ℝ}
    (hfirst : ∀ p ∈ K, p.1 ≤ A)
    (hsecond : ∀ p ∈ K, p.1 = A → p.2 ≤ B)
    (hbound : ∀ p ∈ K, p.2 ≤ M) (hB : 0 ≤ B) (hM : 0 ≤ M)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ p ∈ K, p.2 ≤ B + ε + C * (A - p.1) := by
…

theorem OAI.DoublingHilbert.integral_variance_identity line 88

Source documentation

The variance identity over an arbitrary probability space.

theorem integral_variance_identity {G : X → E} (hG : Integrable G μ)
    (hG2 : Integrable (fun x => ‖G x‖ ^ 2) μ) (a : E) :
    (∫ x, ‖G x - a‖ ^ 2 ∂μ) = (∫ x, ‖G x‖ ^ 2 ∂μ) - ‖a‖ ^ 2 -
      2 * inner ℝ a ((∫ x, G x ∂μ) - a) := by
…

theorem OAI.DoublingHilbert.integrable_norm_sub_sq line 105

theorem OAI.DoublingHilbert.variance_le_of_moments line 112

Source documentation

Small moment error and an upper second moment force small mean-square variation.

theorem variance_le_of_moments {G : X → E} (hG : Integrable G μ)
    (hG2 : Integrable (fun x => ‖G x‖ ^ 2) μ) (a : E) {M : ℝ}
    (hM : (∫ x, ‖G x‖ ^ 2 ∂μ) ≤ M) :
    (∫ x, ‖G x - a‖ ^ 2 ∂μ) ≤ M - ‖a‖ ^ 2 +
      2 * ‖a‖ * ‖(∫ x, G x ∂μ) - a‖ := by
…

theorem OAI.DoublingHilbert.mean_deficit_le line 123

Source documentation

Discarding the nonnegative variance bounds the second-moment deficit.

theorem mean_deficit_le {G : X → E} (hG : Integrable G μ)
    (hG2 : Integrable (fun x => ‖G x‖ ^ 2) μ) (a : E) (A : ℝ) :
    A - (∫ x, ‖G x‖ ^ 2 ∂μ) ≤ A - ‖a‖ ^ 2 +
      2 * ‖a‖ * ‖(∫ x, G x ∂μ) - a‖ := by
…

theorem OAI.DoublingHilbert.integral_second_le_barrier line 134

Source documentation

Integrated affine barrier; unlike a limsup statement, this keeps all quantitative data.

theorem integral_second_le_barrier {K : Set (ℝ × ℝ)} {s t : X → ℝ}
    (hs : Integrable s μ) (ht : Integrable t μ)
    (hvalues : ∀ᵐ x ∂μ, (s x, t x) ∈ K) {A B ε C : ℝ}
    (hbarrier : ∀ p ∈ K, p.2 ≤ B + ε + C * (A - p.1)) :
    (∫ x, t x ∂μ) ≤ B + ε + C * (A - ∫ x, s x ∂μ) := by
…

theorem OAI.DoublingHilbert.vertical_variance_bound line 148

Source documentation

The hard lexicographic energy step, before substituting the geometric moment bounds.

theorem vertical_variance_bound
    {G H : X → E} (hG : Integrable G μ) (hG2 : Integrable (fun x => ‖G x‖ ^ 2) μ)
    (hH : Integrable H μ) (hH2 : Integrable (fun x => ‖H x‖ ^ 2) μ)
    {K : Set (ℝ × ℝ)} (hvalues : ∀ᵐ x ∂μ, (‖G x‖ ^ 2, ‖H x‖ ^ 2) ∈ K)
    {A B ε C D : ℝ} (hC : 0 ≤ C)
    (hbarrier : ∀ p ∈ K, p.2 ≤ B + ε + C * (A - p.1))
    (u v : E) (hu : ‖u‖ ≤ D) (hv : ‖v‖ ≤ D) :
    (∫ x, ‖H x - v‖ ^ 2 ∂μ) ≤ B - ‖v‖ ^ 2 + ε +
      C * (A - ‖u‖ ^ 2 + 2 * D * ‖(∫ x, G x ∂μ) - u‖) +
      2 * D * ‖(∫ x, H x ∂μ) - v‖ := by
…