Documentation

LeanPool.Besicovitch.SixPoint.NormEstimates

Shared norm and quadratic estimates #

The sibling and row-column certificates use the same norm expansions and tangent bounds.

source
theorem LeanPool.Besicovitch.norm_tangent {E : Type u_1} [SeminormedAddCommGroup E] (x : E) {r : ℝ} (hr : 0 < r) :
‖x‖ ≤ (‖x‖ ^ 2 + r ^ 2) / (2 * r)

A norm is bounded by its quadratic tangent at a positive radius.

source
theorem LeanPool.Besicovitch.weighted_norm_tangent {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (weight r : ℝ) (hr : 0 < r) (hweight : 0 ≤ weight) :
weight * ‖x‖ ≤ weight / (2 * r) * (‖x‖ ^ 2 + r ^ 2)

A nonnegative weighted norm is bounded by its quadratic tangent.

source
theorem LeanPool.Besicovitch.weighted_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x y : E) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
‖a • x + b • y‖ ^ 2 = (a + b) * (a * ‖x‖ ^ 2 + b * ‖y‖ ^ 2) - a * b * ‖x - y‖ ^ 2

The squared norm of a nonnegative weighted pair in terms of its separation.

source
theorem LeanPool.Besicovitch.two_mul_norm_tangent {E : Type u_1} [SeminormedAddCommGroup E] (x : E) {r : ℝ} (hr : 0 < r) :
2 * ‖x‖ ≤ r + ‖x‖ ^ 2 / r

Twice a norm is bounded by a positive radius and its squared-norm quotient.

source
theorem LeanPool.Besicovitch.quadratic_le_max_endpoints {a b d l x u : ℝ} (ha : 0 ≤ a) (hlx : l ≤ x) (hxu : x ≤ u) :
a * x ^ 2 + b * x + d ≤ max (a * l ^ 2 + b * l + d) (a * u ^ 2 + b * u + d)

A convex quadratic on an interval is bounded by its endpoint values.

source
theorem LeanPool.Besicovitch.norm_sub_sub_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e x y : E) :
‖e - x - y‖ ^ 2 = ‖e‖ ^ 2 + ‖x‖ ^ 2 + ‖y‖ ^ 2 - 2 * inner ℝ e x - 2 * inner ℝ e y + 2 * inner ℝ x y

Expand the squared norm of a difference of three vectors.

source
def LeanPool.Besicovitch.positivePart (x : ℝ) :
ℝ

The nonnegative part of a real coefficient.

Equations
Instances For
    source
    def LeanPool.Besicovitch.negativePart (x : ℝ) :
    ℝ

    The magnitude of the negative part of a real coefficient.

    Equations
    Instances For
      source
      theorem LeanPool.Besicovitch.positivePart_sub_negativePart (x : ℝ) :
      positivePart x - negativePart x = x

      Positive and negative parts recover the coefficient.

      source
      theorem LeanPool.Besicovitch.positivePart_nonneg (x : ℝ) :
      0 ≤ positivePart x

      The positive part is nonnegative.

      source
      theorem LeanPool.Besicovitch.negativePart_nonneg (x : ℝ) :
      0 ≤ negativePart x

      The negative part is nonnegative.

      source
      theorem LeanPool.Besicovitch.radial_secant {r d l u : ℝ} (hd : 0 ≤ d) (hl : l ≤ r) (hu : r ≤ u) (hsum : 0 < l + u) :
      -d * r ≤ -d / (l + u) * r ^ 2 - d * l * u / (l + u)

      A negative linear radial term is bounded by its quadratic secant.

      source
      theorem LeanPool.Besicovitch.balance_mul_sq_le {a r l u : ℝ} (hl : 0 ≤ l) (hlr : l ≤ r) (hru : r ≤ u) :
      a * r ^ 2 ≤ positivePart a * u ^ 2 - negativePart a * l ^ 2

      Split a signed quadratic coefficient to bound it at the interval endpoints.

      source
      theorem LeanPool.Besicovitch.weightedNorm_le_quadratic {E : Type u_1} [SeminormedAddCommGroup E] (x : E) (weight coefficient : ℝ) (hcoefficient : 0 < coefficient) :
      weight * ‖x‖ ≤ coefficient * ‖x‖ ^ 2 + weight ^ 2 / (4 * coefficient)

      A positive quadratic coefficient gives a global tangent bound for a weighted norm.