Hazard

Local two-child hazard algebra

This file formalizes equations (1), (4), and (5) from hierarchical_quantile_matching.md. The namespace contains only local quantities for a parent with natural-valued child counts x and y.

At an empty parent the paper extends both child hazards by the parent hazard. The policy split is immaterial there; we set it to (1 / 2, 1 / 2), which keeps all q = N * h propagation identities valid without a separate API.

def FD1D.LocalHazard.N (x y : ℕ) : ℝ

The parent count, coerced to ℝ.

Equations

• FD1D.LocalHazard.N x y = ↑x + ↑y

def FD1D.LocalHazard.D (a : ℝ) (x y : ℕ) : ℝ

The denominator D = 2xy + a(x+y) at a nonempty parent.

Equations

• FD1D.LocalHazard.D a x y = 2 * ↑x * ↑y + a * FD1D.LocalHazard.N x y

noncomputable def FD1D.LocalHazard.dL (a : ℝ) (x y : ℕ) : ℝ

The policy's conditional probability of choosing the left child.

Equations

• FD1D.LocalHazard.dL a x y = if x + y = 0 then 1 / 2 else ↑x * (↑y + a) / FD1D.LocalHazard.D a x y

noncomputable def FD1D.LocalHazard.dR (a : ℝ) (x y : ℕ) : ℝ

The policy's conditional probability of choosing the right child.

Equations

• FD1D.LocalHazard.dR a x y = if x + y = 0 then 1 / 2 else ↑y * (↑x + a) / FD1D.LocalHazard.D a x y

noncomputable def FD1D.LocalHazard.hL (a h : ℝ) (x y : ℕ) : ℝ

The left child hazard, including the paper's extension at an empty node.

Equations

• FD1D.LocalHazard.hL a h x y = if x + y = 0 then h else h * FD1D.LocalHazard.N x y * (↑y + a) / FD1D.LocalHazard.D a x y

noncomputable def FD1D.LocalHazard.hR (a h : ℝ) (x y : ℕ) : ℝ

The right child hazard, including the paper's extension at an empty node.

Equations

• FD1D.LocalHazard.hR a h x y = if x + y = 0 then h else h * FD1D.LocalHazard.N x y * (↑x + a) / FD1D.LocalHazard.D a x y

def FD1D.LocalHazard.q (h : ℝ) (x y : ℕ) : ℝ

Parent deletion mass under the invariant q = N h.

Equations

• FD1D.LocalHazard.q h x y = FD1D.LocalHazard.N x y * h

noncomputable def FD1D.LocalHazard.qL (a h : ℝ) (x y : ℕ) : ℝ

Left deletion mass obtained from the policy split.

Equations

• FD1D.LocalHazard.qL a h x y = FD1D.LocalHazard.q h x y * FD1D.LocalHazard.dL a x y

noncomputable def FD1D.LocalHazard.qR (a h : ℝ) (x y : ℕ) : ℝ

Right deletion mass obtained from the policy split.

Equations

• FD1D.LocalHazard.qR a h x y = FD1D.LocalHazard.q h x y * FD1D.LocalHazard.dR a x y

noncomputable def FD1D.LocalHazard.b (a h : ℝ) (x y : ℕ) : ℝ

The signed child-mass imbalance b = q_L - q_R.

Equations

• FD1D.LocalHazard.b a h x y = FD1D.LocalHazard.qL a h x y - FD1D.LocalHazard.qR a h x y

noncomputable def FD1D.LocalHazard.V (a h : ℝ) (x y : ℕ) : ℝ

The average hazard increment in h_L = h + V + w.

Equations

• FD1D.LocalHazard.V a h x y = (FD1D.LocalHazard.hL a h x y + FD1D.LocalHazard.hR a h x y) / 2 - h

noncomputable def FD1D.LocalHazard.w (a h : ℝ) (x y : ℕ) : ℝ

The antisymmetric hazard increment in h_L = h + V + w.

Equations

• FD1D.LocalHazard.w a h x y = (FD1D.LocalHazard.hL a h x y - FD1D.LocalHazard.hR a h x y) / 2

noncomputable def FD1D.LocalHazard.rho (x y : ℕ) : ℝ

The normalized child-count imbalance rho = (x-y)/(x+y).

Equations

• FD1D.LocalHazard.rho x y = (↑x - ↑y) / FD1D.LocalHazard.N x y

noncomputable def FD1D.LocalHazard.t (a p h : ℝ) (x y : ℕ) : ℝ

The parent discrepancy variable t = (p-q)/a.

Equations

• FD1D.LocalHazard.t a p h x y = (p - FD1D.LocalHazard.q h x y) / a

noncomputable def FD1D.LocalHazard.tL (a p h : ℝ) (x y : ℕ) : ℝ

The left child discrepancy variable.

Equations

• FD1D.LocalHazard.tL a p h x y = (p / 2 - FD1D.LocalHazard.qL a h x y) / a

noncomputable def FD1D.LocalHazard.tR (a p h : ℝ) (x y : ℕ) : ℝ

The right child discrepancy variable.

Equations

• FD1D.LocalHazard.tR a p h x y = (p / 2 - FD1D.LocalHazard.qR a h x y) / a

theorem FD1D.LocalHazard.N_nonneg (x y : ℕ) : 0 ≤ N x y

theorem FD1D.LocalHazard.N_pos {x y : ℕ} (hne : x + y ≠ 0) : 0 < N x y

theorem FD1D.LocalHazard.N_ne_zero {x y : ℕ} (hne : x + y ≠ 0) : N x y ≠ 0

theorem FD1D.LocalHazard.count_add_a_pos {a : ℝ} (ha : 0 < a) (k : ℕ) : 0 < ↑k + a

theorem FD1D.LocalHazard.D_pos {a : ℝ} {x y : ℕ} (ha : 0 < a) (hne : x + y ≠ 0) : 0 < D a x y

theorem FD1D.LocalHazard.D_ne_zero {a : ℝ} {x y : ℕ} (ha : 0 < a) (hne : x + y ≠ 0) : D a x y ≠ 0

theorem FD1D.LocalHazard.N_add_two_mul_a_pos {a : ℝ} (ha : 0 < a) (x y : ℕ) : 0 < N x y + 2 * a

theorem FD1D.LocalHazard.N_add_two_mul_a_ne_zero {a : ℝ} (ha : 0 < a) (x y : ℕ) : N x y + 2 * a ≠ 0

theorem FD1D.LocalHazard.dL_add_dR {a : ℝ} {x y : ℕ} (ha : 0 < a) : dL a x y + dR a x y = 1

theorem FD1D.LocalHazard.qL_add_qR {a h : ℝ} {x y : ℕ} (ha : 0 < a) : qL a h x y + qR a h x y = q h x y

theorem FD1D.LocalHazard.q_mul_dL_eq_count_mul_hL {a h qParent : ℝ} {x y : ℕ} (ha : 0 < a) (hq : qParent = N x y * h) : qParent * dL a x y = ↑x * hL a h x y

Algebraic propagation of q = N h to the left child.

theorem FD1D.LocalHazard.q_mul_dR_eq_count_mul_hR {a h qParent : ℝ} {x y : ℕ} (ha : 0 < a) (hq : qParent = N x y * h) : qParent * dR a x y = ↑y * hR a h x y

Algebraic propagation of q = N h to the right child.

theorem FD1D.LocalHazard.qL_eq_count_mul_hL {a h : ℝ} {x y : ℕ} (ha : 0 < a) : qL a h x y = ↑x * hL a h x y

theorem FD1D.LocalHazard.qR_eq_count_mul_hR {a h : ℝ} {x y : ℕ} (ha : 0 < a) : qR a h x y = ↑y * hR a h x y

theorem FD1D.LocalHazard.hL_pos {a h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) : 0 < hL a h x y

theorem FD1D.LocalHazard.hR_pos {a h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) : 0 < hR a h x y

theorem FD1D.LocalHazard.b_eq_neg_a_mul_hazardDiff {a h : ℝ} {x y : ℕ} (ha : 0 < a) : b a h x y = -a * (hL a h x y - hR a h x y)

Equation b = -a(h_L-h_R), including the empty-node extension.

theorem FD1D.LocalHazard.b_eq_neg_two_mul_a_mul_w {a h : ℝ} {x y : ℕ} (ha : 0 < a) : b a h x y = -2 * a * w a h x y

theorem FD1D.LocalHazard.rho_sq_le_one {x y : ℕ} (hne : x + y ≠ 0) : rho x y ^ 2 ≤ 1

theorem FD1D.LocalHazard.hazardIncrement_eq {a h : ℝ} {x y : ℕ} (ha : 0 < a) : (hL a h x y ^ 2 + hR a h x y ^ 2) / 2 - h ^ 2 = b a h x y ^ 2 / a ^ 2 * ((3 - rho x y ^ 2) / 4 + a / N x y)

The exact identity in equation (1).

theorem FD1D.LocalHazard.hazardIncrement_ge {a h : ℝ} {x y : ℕ} (ha : 0 < a) : b a h x y ^ 2 / (2 * a ^ 2) ≤ (hL a h x y ^ 2 + hR a h x y ^ 2) / 2 - h ^ 2

The lower bound in equation (1).

theorem FD1D.LocalHazard.hL_eq_h_add_V_add_w (a h : ℝ) (x y : ℕ) : hL a h x y = h + V a h x y + w a h x y

theorem FD1D.LocalHazard.hR_eq_h_add_V_sub_w (a h : ℝ) (x y : ℕ) : hR a h x y = h + V a h x y - w a h x y

theorem FD1D.LocalHazard.V_eq {a h : ℝ} {x y : ℕ} (ha : 0 < a) : V a h x y = h * (↑x - ↑y) ^ 2 / (2 * D a x y)

theorem FD1D.LocalHazard.w_eq {a h : ℝ} {x y : ℕ} (ha : 0 < a) : w a h x y = h * N x y * (↑y - ↑x) / (2 * D a x y)

theorem FD1D.LocalHazard.V_nonneg {a h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 ≤ h) : 0 ≤ V a h x y

theorem FD1D.LocalHazard.normalizedV_le {a : ℝ} {x y : ℕ} (ha : 0 < a) : (↑x - ↑y) ^ 2 / (2 * D a x y) ≤ N x y / (2 * a)

theorem FD1D.LocalHazard.V_div_h_eq {a h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) : V a h x y / h = (↑x - ↑y) ^ 2 / (2 * D a x y)

theorem FD1D.LocalHazard.V_div_h_le {a h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) : V a h x y / h ≤ N x y / (2 * a)

The bound V/h ≤ N/(2a) from equation (4).

theorem FD1D.LocalHazard.w_sq_eq {a h : ℝ} {x y : ℕ} (ha : 0 < a) : w a h x y ^ 2 = N x y / (N x y + 2 * a) * V a h x y * (h + V a h x y)

The exact quadratic identity for w in equation (4).

theorem FD1D.LocalHazard.N_div_N_add_two_mul_a_nonneg {a : ℝ} (ha : 0 < a) (x y : ℕ) : 0 ≤ N x y / (N x y + 2 * a)

theorem FD1D.LocalHazard.N_div_N_add_two_mul_a_le_one {a : ℝ} (ha : 0 < a) (x y : ℕ) : N x y / (N x y + 2 * a) ≤ 1

theorem FD1D.LocalHazard.abs_w_le_V_add_half_h {a h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 ≤ h) : |w a h x y| ≤ V a h x y + h / 2

theorem FD1D.LocalHazard.tL_eq {a p h : ℝ} {x y : ℕ} (ha : 0 < a) : tL a p h x y = t a p h x y / 2 + w a h x y

The left relation t_L = t/2 + w from equation (4).

theorem FD1D.LocalHazard.tR_eq {a p h : ℝ} {x y : ℕ} (ha : 0 < a) : tR a p h x y = t a p h x y / 2 - w a h x y

The right relation t_R = t/2 - w from equation (4).

theorem FD1D.LocalHazard.tL_le_half_hL {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 ≤ h) (ht : t a p h x y ≤ h / 2) : tL a p h x y ≤ hL a h x y / 2

theorem FD1D.LocalHazard.tR_le_half_hR {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 ≤ h) (ht : t a p h x y ≤ h / 2) : tR a p h x y ≤ hR a h x y / 2

theorem FD1D.LocalHazard.t_div_h_le_half_left {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) (ht : t a p h x y / h ≤ 1 / 2) : tL a p h x y / hL a h x y ≤ 1 / 2

Propagation of the invariant t/h ≤ 1/2 to the left child.

theorem FD1D.LocalHazard.t_div_h_le_half_right {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) (ht : t a p h x y / h ≤ 1 / 2) : tR a p h x y / hR a h x y ≤ 1 / 2

Propagation of the invariant t/h ≤ 1/2 to the right child.

theorem FD1D.LocalHazard.p_le_N_add_half_a_mul_h {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (ht : t a p h x y ≤ h / 2) : p ≤ (N x y + a / 2) * h

The sharper first inequality used in equation (5).

theorem FD1D.LocalHazard.p_le_N_add_a_mul_h {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 ≤ h) (ht : t a p h x y ≤ h / 2) : p ≤ (N x y + a) * h

Equation (5): p ≤ (N+a)h.

theorem FD1D.LocalHazard.p_le_N_add_a_mul_h_of_ratio {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) (ht : t a p h x y / h ≤ 1 / 2) : p ≤ (N x y + a) * h