Integration over the level

Real-variable lemmas with no cube in them. The main statement is level_integration: an inequality between a combination of the functions t ↦ (u - t)⁺ (t - v)⁺ and a combination of indicators of intervals [p, q), valid at every level t, can be integrated over t: ∫ (u - t)⁺ (t - v)⁺ dt = ((u - v)⁺)^3 / 6 and ∫ 1_{[p,q)}(t) dt = (q - p)⁺ (Lemma 7.3 (i) and (ii) of the paper).

theorem AaronsonAmbainis.Level.integral_quad (v u : ℝ) : ∫ (t : ℝ) in v..u, (u - t) * (t - v) = (u - v) ^ 3 / 6

∫_v^u (u - t)(t - v) dt = (u - v)^3 / 6.

theorem AaronsonAmbainis.Level.integral_posParts {a b u v : ℝ} (hub : u ≤ b) (hav : a ≤ v) : ∫ (t : ℝ) in a..b, max (u - t) 0 * max (t - v) 0 = max (u - v) 0 ^ 3 / 6

∫_a^b (u - t)⁺ (t - v)⁺ dt = ((u - v)⁺)^3 / 6 when a ≤ v and u ≤ b (Lemma 7.3 (i) of the paper).

noncomputable def AaronsonAmbainis.Level.stp (c t : ℝ) : ℝ

The step function 1_{c ≤ t}.

Equations

• AaronsonAmbainis.Level.stp c t = if c ≤ t then 1 else 0

theorem AaronsonAmbainis.Level.stp_mono (c : ℝ) : Monotone (stp c)

theorem AaronsonAmbainis.Level.stp_intervalIntegrable (c a b : ℝ) : IntervalIntegrable (stp c) MeasureTheory.volume a b

theorem AaronsonAmbainis.Level.integral_stp {a b c : ℝ} (hac : a ≤ c) (hcb : c ≤ b) : ∫ (t : ℝ) in a..b, stp c t = b - c

∫_a^b 1_{c ≤ t} dt = b - c for c in [a, b] (this gives Lemma 7.3 (ii) of the paper).

theorem AaronsonAmbainis.Level.ind_eq_stp (p q t : ℝ) : (if p ≤ t ∧ t < q then 1 else 0) = stp p t - stp (max p q) t

The indicator of [p, q) as a difference of two step functions.

theorem AaronsonAmbainis.Level.level_integration {α : Type u_1} {β : Type u_2} (s : Finset α) (r : Finset β) (c u v : α → ℝ) (d p q : β → ℝ) (h : ∀ (t : ℝ), ∑ i ∈ s, c i * (max (u i - t) 0 * max (t - v i) 0) ≤ ∑ k ∈ r, d k * if p k ≤ t ∧ t < q k then 1 else 0) : ∑ i ∈ s, c i * (max (u i - v i) 0 ^ 3 / 6) ≤ ∑ k ∈ r, d k * max (q k - p k) 0

Integration over the level. If ∑_i c_i (u_i - t)⁺ (t - v_i)⁺ ≤ ∑_k d_k 1_{[p_k, q_k)}(t) for every real t, then ∑_i c_i ((u_i - v_i)⁺)^3 / 6 ≤ ∑_k d_k (q_k - p_k)⁺. No sign condition on c, d.