ScalarIncrements.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Scalar inequalities for the one-sided coupling estimate

The increasing function couplingPotential m t = (t-m)|t-m|/2 controls squared distances from below and has a trapezoidal increment bound from above. All arguments here are algebraic, by splitting according to the positions of the endpoints relative to the center m.

def OAI.LeanBlast.GotsmanLinial.couplingPotential line 18
Source documentation
The scalar potential used in the one-sided coupling argument.
```
noncomputable def couplingPotential (m t : ℝ) : ℝ :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_self line 21

theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_increment_bounds line 25

Source documentation

Both increment inequalities hold even when the endpoints coincide.

theorem couplingPotential_increment_bounds (m : ℝ) {u v : ℝ} (huv : u ≤ v) :
    (v - u) ^ 2 / 4 ≤ couplingPotential m v - couplingPotential m u ∧
      couplingPotential m v - couplingPotential m u ≤
        (v - u) / 2 * (|u - m| + |v - m|) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.couplingPotential

theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_increment_lower line 52
theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_increment_upper line 56
theorem OAI.LeanBlast.GotsmanLinial.monotone_couplingPotential line 61
theorem OAI.LeanBlast.GotsmanLinial.strictMono_couplingPotential line 66
theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_le_iff line 72
theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_lt_iff line 76
theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_eq_iff line 80
theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_sub_nonneg_iff line 84
theorem OAI.LeanBlast.GotsmanLinial.couplingPotential_sub_pos_iff line 88
theorem OAI.LeanBlast.GotsmanLinial.abs_couplingPotential_sub_of_le line 92
theorem OAI.LeanBlast.GotsmanLinial.sq_sub_le_four_mul_abs_potential_sub line 99
Source documentation
The pointwise lower bound in the coupling argument, without ordering the two real variables.
```
theorem sq_sub_le_four_mul_abs_potential_sub (m u v : ℝ) :
    (u - v) ^ 2 ≤ 4 * |couplingPotential m u - couplingPotential m v| := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.couplingPotential
theorem OAI.LeanBlast.GotsmanLinial.max_couplingPotential_increment_le line 111
Source documentation
An upper bound for the positive part of a potential increment under a one-sided bound on the original increment.
```
theorem max_couplingPotential_increment_le (m a u v : ℝ)
    (ha : 0 ≤ a) (hstep : v - u ≤ a) :
    max (couplingPotential m v - couplingPotential m u) 0 ≤
      a / 2 * (|u - m| + |v - m|) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.couplingPotential