Physlib

PhyslibAlpha.Mathematics.Analysis.RealBounds

Elementary real bounds

i. Overview

Three elementary estimates for real numbers: suprema of sums over a codirected family, inequalities up to `1 / (n + 1)` for every `n`, and averages that put almost all weight on one term.

ii. Key results

- `Real.ciSup_add` : suprema add along a family in which any two indices are dominated by a third. - `Real.le_of_forall_nat_le_add` : `a ≤ b` if `a ≤ b + 1 / (n + 1)` for every `n`. - `Real.abs_sum_mul_sub_le` : an average with weight at least `1 - θ` on one term is within `2 * A * θ` of it, for terms bounded by `A`.

iii. Table of contents

  • A. Suprema
  • B. Averages

A. Suprema

B. Averages

3 declarations

theorem

sup⁡i(fi+gi)=sup⁡ifi+sup⁡igi\sup_{i} (f_i + g_i) = \sup_{i} f_i + \sup_{i} g_i for Codirected Families

Let ι\iota be a non-empty index set, and let f,g:ι→Rf, g: \iota \to \mathbb{R} be two functions such that their ranges are bounded above. Suppose that for every i,j∈ιi, j \in \iota, there exists an index k∈ιk \in \iota such that f(i)≤f(k)f(i) \le f(k) and g(j)≤g(k)g(j) \le g(k). Then the supremum of the sum of the functions is equal to the sum of their individual suprema: sup⁡i∈ι(f(i)+g(i))=sup⁡i∈ιf(i)+sup⁡i∈ιg(i)\sup_{i \in \iota} (f(i) + g(i)) = \sup_{i \in \iota} f(i) + \sup_{i \in \iota} g(i)

theorem

(∀n∈N,a≤b+1n+1)  ⟹  a≤b(\forall n \in \mathbb{N}, a \leq b + \frac{1}{n+1}) \implies a \leq b

Let aa and bb be real numbers. If a≤b+1n+1a \le b + \frac{1}{n + 1} for every natural number n∈Nn \in \mathbb{N}, then a≤ba \le b.

theorem

∣∑clql−ci∣≤2Aθ|\sum c_l q_l - c_i| \le 2 A \theta when qi≥1−θq_i \ge 1 - \theta for bounded clc_l

Let ι\iota be a finite set. Let q:ι→Rq: \iota \to \mathbb{R} be a collection of non-negative weights that sum to 1, i.e., ql≥0q_l \ge 0 for all l∈ιl \in \iota and ∑l∈ιql=1\sum_{l \in \iota} q_l = 1. Let c:ι→Rc: \iota \to \mathbb{R} be a collection of values such that ∣cl∣≤A|c_l| \le A for some A∈RA \in \mathbb{R}. If there exists an index i∈ιi \in \iota and a value θ∈R\theta \in \mathbb{R} such that the weight qiq_i satisfies 1−θ≤qi1 - \theta \le q_i, then the absolute difference between the weighted average and cic_i is bounded as follows: ∣∑l∈ιclql−ci∣≤2Aθ \left| \sum_{l \in \iota} c_l q_l - c_i \right| \le 2 A \theta