Fully dynamic matching on the line

Common definitions for the formal proof of the hierarchical quantile matching bound. All analytic quantities are represented in ℝ; finite probability laws are represented by weighted sums over finite types.

noncomputable def FD1D.policyA (m : ℕ) : ℕ

The regularizing parameter used by the policy.

Equations

• FD1D.policyA m = 200 * ⌈Real.logb 2 (↑m + 1)⌉₊

structure FD1D.FiniteLaw (α : Type u_1) [Fintype α] : Type u_1

A probability mass function on a finite type, represented without quotienting.

• mass : α → ℝ

  Probability mass assigned to each point of the finite state space.

• mass_nonneg (x : α) : 0 ≤ self.mass x
• sum_mass : ∑ x : α, self.mass x = 1

def FD1D.FiniteLaw.expect {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (f : α → ℝ) : ℝ

Expectation of a real observable under the finite law.

Equations

• μ.expect f = ∑ x : α, μ.mass x * f x

@[simp]

theorem FD1D.FiniteLaw.expect_const {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (c : ℝ) : (μ.expect fun (x : α) => c) = c

theorem FD1D.FiniteLaw.expect_nonneg {α : Type u_1} [Fintype α] (μ : FiniteLaw α) {f : α → ℝ} (hf : ∀ (x : α), 0 ≤ f x) : 0 ≤ μ.expect f

theorem FD1D.FiniteLaw.expect_mono {α : Type u_1} [Fintype α] (μ : FiniteLaw α) {f g : α → ℝ} (hfg : ∀ (x : α), f x ≤ g x) : μ.expect f ≤ μ.expect g