Transport

Dyadic Haar transport on the unit interval

This file isolates the analytic part of Section 2. A DyadicMass L is a binary tree with exactly 2^L leaf masses. Its recursive CDF is the CDF of the measure which spreads every leaf mass uniformly over its dyadic cell.

The second half of the file proves the finite-family Haar calculation. Tree symmetry is expressed by mass-preserving child-swap equivalences on the finite state space. This is exactly the property used to kill a nested cross term; disjoint tents vanish pointwise.

inductive FD1D.DyadicMass : ℕ → Type

A complete binary tree of 2^L real leaf masses.

• leaf (mass : ℝ) : DyadicMass 0
• branch {L : ℕ} (left right : DyadicMass L) : DyadicMass (L + 1)

def FD1D.DyadicMass.total {L : ℕ} : DyadicMass L → ℝ

Total mass below the root.

Equations

• (FD1D.DyadicMass.leaf m).total = m
• (l.branch r).total = l.total + r.total

def FD1D.DyadicMass.leaves {L : ℕ} : DyadicMass L → List ℝ

Leaf masses, in their left-to-right spatial order.

Equations

• (FD1D.DyadicMass.leaf m).leaves = [m]
• (l.branch r).leaves = l.leaves ++ r.leaves

@[simp]

theorem FD1D.DyadicMass.length_leaves {L : ℕ} (q : DyadicMass L) : q.leaves.length = 2 ^ L

def FD1D.DyadicMass.ofLeafVector (L : ℕ) : (Fin (2 ^ L) → ℝ) → DyadicMass L

Build the complete dyadic mass tree from its left-to-right vector of 2^L leaf masses.

Equations

• One or more equations did not get rendered due to their size.
• FD1D.DyadicMass.ofLeafVector 0 f = FD1D.DyadicMass.leaf (f 0)

@[simp]

theorem FD1D.DyadicMass.total_ofLeafVector (L : ℕ) (f : Fin (2 ^ L) → ℝ) : (ofLeafVector L f).total = ∑ i : Fin (2 ^ L), f i

def FD1D.DyadicMass.allNonneg {L : ℕ} : DyadicMass L → Prop

Every leaf mass is nonnegative.

Equations

• (FD1D.DyadicMass.leaf m).allNonneg = (0 ≤ m)
• (l.branch r).allNonneg = (l.allNonneg ∧ r.allNonneg)

theorem FD1D.DyadicMass.allNonneg_ofLeafVector (L : ℕ) (f : Fin (2 ^ L) → ℝ) (hf : ∀ (i : Fin (2 ^ L)), 0 ≤ f i) : (ofLeafVector L f).allNonneg

theorem FD1D.DyadicMass.total_nonneg {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) : 0 ≤ q.total

structure FD1D.DyadicMass.IsProbability {L : ℕ} (q : DyadicMass L) : Prop

The hypotheses saying that the 2^L leaf masses form a probability vector.

• nonneg : q.allNonneg
• total_eq_one : q.total = 1

theorem FD1D.DyadicMass.isProbability_ofLeafVector (L : ℕ) (f : Fin (2 ^ L) → ℝ) (hf : ∀ (i : Fin (2 ^ L)), 0 ≤ f i) (hsum : ∑ i : Fin (2 ^ L), f i = 1) : (ofLeafVector L f).IsProbability

def FD1D.DyadicMass.piecewiseCDF {L : ℕ} : DyadicMass L → ℝ → ℝ

The explicit piecewise-linear CDF. Outside [0,1] this is merely a piecewise-linear extension; all CDF statements below are restricted to the unit interval.

Equations

• (FD1D.DyadicMass.leaf m).piecewiseCDF = fun (z : ℝ) => m * z
• (l.branch r).piecewiseCDF = fun (z : ℝ) => if z ≤ 1 / 2 then l.piecewiseCDF (2 * z) else l.total + r.piecewiseCDF (2 * z - 1)

@[simp]

theorem FD1D.DyadicMass.piecewiseCDF_zero {L : ℕ} (q : DyadicMass L) : q.piecewiseCDF 0 = 0

@[simp]

theorem FD1D.DyadicMass.piecewiseCDF_one {L : ℕ} (q : DyadicMass L) : q.piecewiseCDF 1 = q.total

theorem FD1D.DyadicMass.piecewiseCDF_nonneg {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {z : ℝ} (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : 0 ≤ q.piecewiseCDF z

theorem FD1D.DyadicMass.piecewiseCDF_le_total {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {z : ℝ} (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : q.piecewiseCDF z ≤ q.total

theorem FD1D.DyadicMass.piecewiseCDF_monotoneOn {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) : MonotoneOn q.piecewiseCDF (Set.Icc 0 1)

Nonnegative leaf masses make the explicit CDF monotone on [0,1].

def FD1D.DyadicMass.quantile {L : ℕ} : DyadicMass L → ℝ → ℝ

The explicit generalized inverse in mass coordinates. Its input ranges from 0 to q.total; at a branch the interval is split at the left mass.

Equations

• (FD1D.DyadicMass.leaf m).quantile = fun (u : ℝ) => u / m
• (l.branch r).quantile = fun (u : ℝ) => if u ≤ l.total then l.quantile u / 2 else (1 + r.quantile (u - l.total)) / 2

def FD1D.DyadicMass.selectedLeaf {L : ℕ} : DyadicMass L → ℝ → ℝ

The actual selected-leaf policy. It returns the left endpoint of the leaf whose cumulative-mass interval contains u.

Equations

• (FD1D.DyadicMass.leaf m).selectedLeaf = fun (x : ℝ) => 0
• (l.branch r).selectedLeaf = fun (u : ℝ) => if u ≤ l.total then l.selectedLeaf u / 2 else (1 + r.selectedLeaf (u - l.total)) / 2

theorem FD1D.DyadicMass.piecewiseCDF_measurable {L : ℕ} (q : DyadicMass L) : Measurable q.piecewiseCDF

theorem FD1D.DyadicMass.quantile_measurable {L : ℕ} (q : DyadicMass L) : Measurable q.quantile

theorem FD1D.DyadicMass.selectedLeaf_measurable {L : ℕ} (q : DyadicMass L) : Measurable q.selectedLeaf

theorem FD1D.DyadicMass.quantile_mem_unit {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ q.total) : q.quantile u ∈ Set.Icc 0 1

The explicit generalized inverse takes mass coordinates into [0,1].

theorem FD1D.DyadicMass.selectedLeaf_mem_unit {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ q.total) : q.selectedLeaf u ∈ Set.Icc 0 1

The selected point is an endpoint in the unit interval.

theorem FD1D.DyadicMass.quantile_pos {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {u : ℝ} (hu0 : 0 < u) (hu1 : u ≤ q.total) : 0 < q.quantile u

Positive mass coordinates have a strictly positive generalized inverse.

theorem FD1D.DyadicMass.quantile_le_iff {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {u z : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ q.total) (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : q.quantile u ≤ z ↔ u ≤ q.piecewiseCDF z

Generalized-inverse relation for the explicit recursive map. This includes zero-mass leaves and therefore does not require strict positivity.

theorem FD1D.DyadicMass.selectedLeaf_sub_quantile_le {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ q.total) : |q.selectedLeaf u - q.quantile u| ≤ 1 / ↑(2 ^ L)

The selected leaf endpoint and the continuous quantile lie in the same depth-L dyadic cell.

noncomputable def FD1D.DyadicMass.unitTent (z : ℝ) : ℝ

The height-1/2 tent on the unit interval, in local coordinates.

Equations

• FD1D.DyadicMass.unitTent z = if z ≤ 1 / 2 then z else 1 - z

def FD1D.DyadicMass.haarSeries {L : ℕ} : DyadicMass L → ℝ → ℝ

The integrated Haar series, written recursively. At a branch it adds the root imbalance and then evaluates the unique child series whose support contains z.

Equations

• (FD1D.DyadicMass.leaf m).haarSeries = fun (x : ℝ) => 0
• (l.branch r).haarSeries = fun (z : ℝ) => (l.total - r.total) * FD1D.DyadicMass.unitTent z + if z ≤ 1 / 2 then l.haarSeries (2 * z) else r.haarSeries (2 * z - 1)

theorem FD1D.DyadicMass.cdf_sub_linear_eq_haar {L : ℕ} (q : DyadicMass L) {z : ℝ} (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : q.piecewiseCDF z - q.total * z = q.haarSeries z

Pointwise integrated Haar expansion of the explicit piecewise-linear CDF.

Dyadic tents and their elementary integrals

noncomputable def FD1D.dyadicTent (l p z : ℝ) : ℝ

The height-1/2 tent on [l,l+p]. Splitting into Icc and Ioc makes the two affine pieces disjoint without changing any Lebesgue integral.

Equations

• FD1D.dyadicTent l p z = (Set.Icc l (l + p / 2)).indicator (fun (x : ℝ) => (x - l) / p) z + (Set.Ioc (l + p / 2) (l + p)).indicator (fun (x : ℝ) => (l + p - x) / p) z

theorem FD1D.dyadicTent_eq_zero_of_not_mem {l p z : ℝ} (hp : 0 ≤ p) (hz : z ∉ Set.Icc l (l + p)) : dyadicTent l p z = 0

theorem FD1D.dyadicTent_ne_zero_mem_Ioo {l p z : ℝ} (hp : 0 < p) (hz : dyadicTent l p z ≠ 0) : z ∈ Set.Ioo l (l + p)

A nonzero tent value lies in the interior of its supporting interval.

theorem FD1D.dyadicTent_sq_integral (l p : ℝ) (hp : 0 < p) : ∫ (z : ℝ), dyadicTent l p z ^ 2 = p / 12

The exact tent normalization used in Section 2: ∫ tau_v² = p_v/12.

theorem FD1D.dyadicTent_mul_eq_zero_of_separated {l₁ p₁ l₂ p₂ z : ℝ} (hp₁ : 0 < p₁) (hp₂ : 0 < p₂) (hsep : l₁ + p₁ ≤ l₂ ∨ l₂ + p₂ ≤ l₁) : dyadicTent l₁ p₁ z * dyadicTent l₂ p₂ z = 0

Tents with separated interiors have zero pointwise product.

theorem FD1D.dyadicTent_stronglyMeasurable (l p : ℝ) : MeasureTheory.StronglyMeasurable (dyadicTent l p)

theorem FD1D.dyadicTent_integrable (l p : ℝ) : MeasureTheory.Integrable (dyadicTent l p) MeasureTheory.volume

theorem FD1D.abs_dyadicTent_le_half (l p z : ℝ) (hp : 0 < p) : |dyadicTent l p z| ≤ 1 / 2

theorem FD1D.dyadicTent_mul_integrable (l₁ p₁ l₂ p₂ : ℝ) (hp₁ : 0 < p₁) : MeasureTheory.Integrable (fun (z : ℝ) => dyadicTent l₁ p₁ z * dyadicTent l₂ p₂ z) MeasureTheory.volume

Flattening the recursive Haar series

structure FD1D.HaarTerm : Type

One internal-node term in the integrated Haar expansion.

• left : ℝ

  Left endpoint of the dyadic interval supporting the Haar term.

• width : ℝ

  Width of the interval supporting the Haar term.

• coeff : ℝ

  Coefficient multiplying the integrated Haar tent.

noncomputable def FD1D.HaarTerm.value (t : HaarTerm) (z : ℝ) : ℝ

Pointwise value of one geometric integrated Haar term.

Equations

• t.value z = t.coeff * FD1D.dyadicTent t.left t.width z

noncomputable def FD1D.haarTermSum (ts : List HaarTerm) (z : ℝ) : ℝ

Pointwise value of a finite list of integrated Haar terms.

Equations

• FD1D.haarTermSum ts z = (List.map (fun (t : FD1D.HaarTerm) => t.value z) ts).sum

@[simp]

theorem FD1D.haarTermSum_nil (z : ℝ) : haarTermSum [] z = 0

@[simp]

theorem FD1D.haarTermSum_cons (t : HaarTerm) (ts : List HaarTerm) (z : ℝ) : haarTermSum (t :: ts) z = t.value z + haarTermSum ts z

@[simp]

theorem FD1D.haarTermSum_append (s t : List HaarTerm) (z : ℝ) : haarTermSum (s ++ t) z = haarTermSum s z + haarTermSum t z

def FD1D.DyadicMass.haarTermsAt {L : ℕ} : ℝ → ℝ → DyadicMass L → List HaarTerm

List every internal node, placing the root on [a,a+p] and recursively placing the two child lists on its two halves. The coefficient at each node is exactly its left-subtree mass minus its right-subtree mass.

Equations

• One or more equations did not get rendered due to their size.
• FD1D.DyadicMass.haarTermsAt x✝¹ x✝ (FD1D.DyadicMass.leaf mass) = []

noncomputable def FD1D.DyadicMass.haarTerms {L : ℕ} (q : DyadicMass L) : List HaarTerm

The internal-node Haar terms in their geometric locations in [0,1].

Equations

• q.haarTerms = FD1D.DyadicMass.haarTermsAt 0 1 q

@[simp]

theorem FD1D.DyadicMass.length_haarTermsAt {L : ℕ} (q : DyadicMass L) (a p : ℝ) : (haarTermsAt a p q).length = 2 ^ L - 1

@[simp]

theorem FD1D.DyadicMass.length_haarTerms {L : ℕ} (q : DyadicMass L) : q.haarTerms.length = 2 ^ L - 1

theorem FD1D.DyadicMass.haarTermsAt_width_pos {L : ℕ} (q : DyadicMass L) {a p : ℝ} (hp : 0 < p) {t : HaarTerm} (ht : t ∈ haarTermsAt a p q) : 0 < t.width

theorem FD1D.DyadicMass.haarTerms_width_pos {L : ℕ} (q : DyadicMass L) {t : HaarTerm} (ht : t ∈ q.haarTerms) : 0 < t.width

theorem FD1D.DyadicMass.haarSeries_eq_haarTermSumAt {L : ℕ} (q : DyadicMass L) {a p z : ℝ} (hp : 0 < p) (hz0 : a ≤ z) (hz1 : z ≤ a + p) : q.haarSeries ((z - a) / p) = haarTermSum (haarTermsAt a p q) z

The recursive integrated Haar series is the sum of every internal-node coefficient times its geometric tent, on any positive ambient interval.

theorem FD1D.DyadicMass.haarSeries_eq_haarTermSum {L : ℕ} (q : DyadicMass L) {z : ℝ} (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : q.haarSeries z = haarTermSum q.haarTerms z

Pointwise finite internal-node expansion on [0,1].

Geometric support and nesting vocabulary

@[reducible, inline]

abbrev FD1D.CompleteHaarNode (L : ℕ) : Type

Internal nodes of a depth-L complete binary tree.

Equations

• FD1D.CompleteHaarNode L = ((d : Fin L) × Fin (2 ^ ↑d))

noncomputable def FD1D.haarNodeLeft {L : ℕ} (v : CompleteHaarNode L) : ℝ

Left endpoint of the dyadic interval indexed by a complete Haar node.

Equations

• FD1D.haarNodeLeft v = ↑↑v.snd / ↑(2 ^ ↑v.fst)

noncomputable def FD1D.haarNodeWidth {L : ℕ} (v : CompleteHaarNode L) : ℝ

Width of the dyadic interval indexed by a complete Haar node.

Equations

• FD1D.haarNodeWidth v = 1 / ↑(2 ^ ↑v.fst)

noncomputable def FD1D.haarNodeTent {L : ℕ} (v : CompleteHaarNode L) : ℝ → ℝ

Integrated Haar tent on the interval indexed by the node.

Equations

• FD1D.haarNodeTent v = FD1D.dyadicTent (FD1D.haarNodeLeft v) (FD1D.haarNodeWidth v)

theorem FD1D.haarNodeWidth_pos {L : ℕ} (v : CompleteHaarNode L) : 0 < haarNodeWidth v

def FD1D.HaarSupportNested {L : ℕ} (v w : CompleteHaarNode L) : Prop

Geometric nesting of two dyadic node supports.

Equations

• FD1D.HaarSupportNested v w = (Set.Icc (FD1D.haarNodeLeft v) (FD1D.haarNodeLeft v + FD1D.haarNodeWidth v) ⊆ Set.Icc (FD1D.haarNodeLeft w) (FD1D.haarNodeLeft w + FD1D.haarNodeWidth w))

theorem FD1D.haarNodeTent_eq_zero_outside {L : ℕ} (v : CompleteHaarNode L) {z : ℝ} (hz : z ∉ Set.Icc (haarNodeLeft v) (haarNodeLeft v + haarNodeWidth v)) : haarNodeTent v z = 0

theorem FD1D.HaarSupportNested.trans {L : ℕ} {u v w : CompleteHaarNode L} (huv : HaarSupportNested u v) (hvw : HaarSupportNested v w) : HaarSupportNested u w

Canonical complete-tree indexing

def FD1D.DyadicMass.nodeChildMasses {L : ℕ} : DyadicMass L → CompleteHaarNode L → ℝ × ℝ

The masses of the two children of an internal node v = ⟨d,k⟩. At positive depth, k selects the appropriate half-tree recursively.

Equations

• One or more equations did not get rendered due to their size.
• (FD1D.DyadicMass.leaf mass).nodeChildMasses v = v.fst.elim0
• (l.branch r).nodeChildMasses ⟨⟨0, isLt⟩, snd⟩ = (l.total, r.total)

def FD1D.DyadicMass.nodeCoefficient {L : ℕ} (q : DyadicMass L) (v : CompleteHaarNode L) : ℝ

The Haar coefficient at a node is its left-child mass minus its right-child mass.

Equations

• q.nodeCoefficient v = (q.nodeChildMasses v).1 - (q.nodeChildMasses v).2

theorem FD1D.DyadicMass.nodeCoefficient_eq_childMass_sub {L : ℕ} (q : DyadicMass L) (v : CompleteHaarNode L) : q.nodeCoefficient v = (q.nodeChildMasses v).1 - (q.nodeChildMasses v).2

@[simp]

theorem FD1D.DyadicMass.nodeChildMasses_root {L : ℕ} (l r : DyadicMass L) : (l.branch r).nodeChildMasses ⟨0, 0⟩ = (l.total, r.total)

@[simp]

theorem FD1D.DyadicMass.nodeCoefficient_root {L : ℕ} (l r : DyadicMass L) : (l.branch r).nodeCoefficient ⟨0, 0⟩ = l.total - r.total

def FD1D.DyadicMass.leftNode {L : ℕ} (v : CompleteHaarNode L) : CompleteHaarNode (L + 1)

Embed a node into the left half-tree one level below a new root.

Equations

• FD1D.DyadicMass.leftNode v = ⟨v.fst.succ, ⟨↑v.snd, ⋯⟩⟩

def FD1D.DyadicMass.rightNode {L : ℕ} (v : CompleteHaarNode L) : CompleteHaarNode (L + 1)

Embed a node into the right half-tree one level below a new root.

Equations

• FD1D.DyadicMass.rightNode v = ⟨v.fst.succ, ⟨2 ^ ↑v.fst + ↑v.snd, ⋯⟩⟩

def FD1D.DyadicMass.childFinEquiv (d : ℕ) : Fin (2 ^ d + 2 ^ d) ≃ Fin (2 ^ (d + 1))

Identification of the two child index blocks with the next dyadic level.

Equations

• FD1D.DyadicMass.childFinEquiv d = finCongr ⋯

theorem FD1D.DyadicMass.succNode_castAdd_eq_leftNode {L : ℕ} (d : Fin L) (v : Fin (2 ^ ↑d)) : ⟨d.succ, (childFinEquiv ↑d) (Fin.castAdd (2 ^ ↑d) v)⟩ = leftNode ⟨d, v⟩

theorem FD1D.DyadicMass.succNode_natAdd_eq_rightNode {L : ℕ} (d : Fin L) (v : Fin (2 ^ ↑d)) : ⟨d.succ, (childFinEquiv ↑d) (Fin.natAdd (2 ^ ↑d) v)⟩ = rightNode ⟨d, v⟩

@[simp]

theorem FD1D.DyadicMass.haarNodeLeft_leftNode {L : ℕ} (v : CompleteHaarNode L) : haarNodeLeft (leftNode v) = haarNodeLeft v / 2

@[simp]

theorem FD1D.DyadicMass.haarNodeWidth_leftNode {L : ℕ} (v : CompleteHaarNode L) : haarNodeWidth (leftNode v) = haarNodeWidth v / 2

@[simp]

theorem FD1D.DyadicMass.haarNodeLeft_rightNode {L : ℕ} (v : CompleteHaarNode L) : haarNodeLeft (rightNode v) = 1 / 2 + haarNodeLeft v / 2

@[simp]

theorem FD1D.DyadicMass.haarNodeWidth_rightNode {L : ℕ} (v : CompleteHaarNode L) : haarNodeWidth (rightNode v) = haarNodeWidth v / 2

@[simp]

theorem FD1D.DyadicMass.nodeChildMasses_leftNode {L : ℕ} (l r : DyadicMass L) (v : CompleteHaarNode L) : (l.branch r).nodeChildMasses (leftNode v) = l.nodeChildMasses v

@[simp]

theorem FD1D.DyadicMass.nodeChildMasses_rightNode {L : ℕ} (l r : DyadicMass L) (v : CompleteHaarNode L) : (l.branch r).nodeChildMasses (rightNode v) = r.nodeChildMasses v

@[simp]

theorem FD1D.DyadicMass.nodeCoefficient_leftNode {L : ℕ} (l r : DyadicMass L) (v : CompleteHaarNode L) : (l.branch r).nodeCoefficient (leftNode v) = l.nodeCoefficient v

@[simp]

theorem FD1D.DyadicMass.nodeCoefficient_rightNode {L : ℕ} (l r : DyadicMass L) (v : CompleteHaarNode L) : (l.branch r).nodeCoefficient (rightNode v) = r.nodeCoefficient v

Finite tree symmetry and cancellation of cross terms

def FD1D.FiniteLaw.InvariantUnder {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (e : Ω ≃ Ω) : Prop

A finite law is invariant under a state-space equivalence.

Equations

• μ.InvariantUnder e = ∀ (ω : Ω), μ.mass (e ω) = μ.mass ω

def FD1D.FiniteLaw.OddSymmetry {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (f : Ω → ℝ) : Prop

An observable has an odd symmetry if a mass-preserving child swap changes its sign. A local tree automorphism supplies precisely such an equivalence for an ancestor-descendant coefficient product.

Equations

• μ.OddSymmetry f = ∃ (e : Ω ≃ Ω), μ.InvariantUnder e ∧ ∀ (ω : Ω), f (e ω) = -f ω

theorem FD1D.FiniteLaw.expect_comp_equiv {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (e : Ω ≃ Ω) (he : μ.InvariantUnder e) (f : Ω → ℝ) : (μ.expect fun (ω : Ω) => f (e ω)) = μ.expect f

theorem FD1D.FiniteLaw.expect_eq_zero_of_oddSymmetry {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (f : Ω → ℝ) (hodd : μ.OddSymmetry f) : μ.expect f = 0

A mass-preserving sign flip forces expectation zero.

def FD1D.IntervalsSeparated {ι : Type u_1} (l p : ι → ℝ) (i j : ι) : Prop

The interiors of two tent supports are disjoint (endpoints may coincide).

Equations

• FD1D.IntervalsSeparated l p i j = (l i + p i ≤ l j ∨ l j + p j ≤ l i)

noncomputable def FD1D.haarCombination {ι : Type u_1} [Fintype ι] (l p b : ι → ℝ) (z : ℝ) : ℝ

A finite integrated Haar expansion.

Equations

• FD1D.haarCombination l p b z = ∑ i : ι, b i * FD1D.dyadicTent (l i) (p i) z

theorem FD1D.DyadicMass.branch_succ_fiber {L : ℕ} (l r : DyadicMass L) (d : Fin L) (z : ℝ) : ∑ y : Fin (2 ^ ↑d.succ), (l.branch r).nodeCoefficient ⟨d.succ, y⟩ * dyadicTent (haarNodeLeft ⟨d.succ, y⟩) (haarNodeWidth ⟨d.succ, y⟩) z = ∑ y : Fin (2 ^ ↑d), l.nodeCoefficient ⟨d, y⟩ * dyadicTent (haarNodeLeft (leftNode ⟨d, y⟩)) (haarNodeWidth (leftNode ⟨d, y⟩)) z + ∑ y : Fin (2 ^ ↑d), r.nodeCoefficient ⟨d, y⟩ * dyadicTent (haarNodeLeft (rightNode ⟨d, y⟩)) (haarNodeWidth (rightNode ⟨d, y⟩)) z

theorem FD1D.DyadicMass.dyadicTent_scale_left (l p z : ℝ) (hp : p ≠ 0) : dyadicTent (l / 2) (p / 2) z = dyadicTent l p (2 * z)

theorem FD1D.DyadicMass.dyadicTent_scale_right (l p z : ℝ) (hp : p ≠ 0) : dyadicTent (1 / 2 + l / 2) (p / 2) z = dyadicTent l p (2 * z - 1)

theorem FD1D.DyadicMass.haarCombination_leftNode {L : ℕ} (b : CompleteHaarNode L → ℝ) (z : ℝ) : ∑ v : CompleteHaarNode L, b v * dyadicTent (haarNodeLeft (leftNode v)) (haarNodeWidth (leftNode v)) z = haarCombination haarNodeLeft haarNodeWidth b (2 * z)

theorem FD1D.DyadicMass.haarCombination_rightNode {L : ℕ} (b : CompleteHaarNode L → ℝ) (z : ℝ) : ∑ v : CompleteHaarNode L, b v * dyadicTent (haarNodeLeft (rightNode v)) (haarNodeWidth (rightNode v)) z = haarCombination haarNodeLeft haarNodeWidth b (2 * z - 1)

theorem FD1D.DyadicMass.haarNodeLeft_nonneg {L : ℕ} (v : CompleteHaarNode L) : 0 ≤ haarNodeLeft v

theorem FD1D.DyadicMass.haarNodeRight_le_one {L : ℕ} (v : CompleteHaarNode L) : haarNodeLeft v + haarNodeWidth v ≤ 1

theorem FD1D.DyadicMass.haarCombination_eq_zero_of_outside {L : ℕ} (b : CompleteHaarNode L → ℝ) {z : ℝ} (hz : z ≤ 0 ∨ 1 ≤ z) : haarCombination haarNodeLeft haarNodeWidth b z = 0

theorem FD1D.DyadicMass.branch_root_fiber {L : ℕ} (l r : DyadicMass L) (z : ℝ) : ∑ y : Fin (2 ^ ↑0), (l.branch r).nodeCoefficient ⟨0, y⟩ * dyadicTent (haarNodeLeft ⟨0, y⟩) (haarNodeWidth ⟨0, y⟩) z = (l.total - r.total) * dyadicTent 0 1 z

theorem FD1D.DyadicMass.haarSeries_eq_haarCombination {L : ℕ} (q : DyadicMass L) {z : ℝ} (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : q.haarSeries z = haarCombination haarNodeLeft haarNodeWidth q.nodeCoefficient z

The recursive Haar series is exactly the canonical finite sum over all internal nodes ⟨d,k⟩ of the complete depth-L tree.

theorem FD1D.DyadicMass.cdf_sub_linear_eq_haarCombination {L : ℕ} (q : DyadicMass L) {z : ℝ} (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : q.piecewiseCDF z - q.total * z = haarCombination haarNodeLeft haarNodeWidth q.nodeCoefficient z

The canonical node sum is the CDF deviation on the unit interval.

noncomputable def FD1D.haarL2 {ι : Type u_1} [Fintype ι] (l p b : ι → ℝ) : ℝ

Squared L² norm of a finite integrated Haar expansion.

Equations

• FD1D.haarL2 l p b = ∫ (z : ℝ), FD1D.haarCombination l p b z ^ 2

theorem FD1D.haarL2_eq_gram {ι : Type u_1} [Fintype ι] (l p b : ι → ℝ) (hp : ∀ (i : ι), 0 < p i) : haarL2 l p b = ∑ i : ι, ∑ j : ι, b i * b j * ∫ (z : ℝ), dyadicTent (l i) (p i) z * dyadicTent (l j) (p j) z

theorem FD1D.expected_haarL2 {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [Fintype Ω] (μ : FiniteLaw Ω) (l p : ι → ℝ) (b : Ω → ι → ℝ) (hp : ∀ (i : ι), 0 < p i) (hsym : ∀ (i j : ι), i ≠ j → IntervalsSeparated l p i j ∨ μ.OddSymmetry fun (ω : Ω) => b ω i * b ω j) : (μ.expect fun (ω : Ω) => haarL2 l p (b ω)) = 1 / 12 * ∑ i : ι, p i * μ.expect fun (ω : Ω) => b ω i ^ 2

Expected Parseval identity for integrated Haar functions. For unequal nodes, either their interiors are disjoint or a tree child swap makes the coefficient product odd. Thus every cross term vanishes.

Quantile/CDF cost and Cauchy--Schwarz

noncomputable def FD1D.cdfTransportArea (f : ℝ → ℝ) : ℝ

The elementary one-dimensional monotone-transport cost: the area between the source and target CDFs. This representation avoids introducing a separate Wasserstein API.

Equations

• FD1D.cdfTransportArea f = ∫ (z : ℝ) in Set.Icc 0 1, |f z|

theorem FD1D.integral_abs_quantile_sub_id_eq_integral_abs_cdf_sub_id {F T : ℝ → ℝ} (_hF : Measurable F) (hT : Measurable T) (hF01 : Set.MapsTo F (Set.Icc 0 1) (Set.Icc 0 1)) (hT01 : Set.MapsTo T (Set.Icc 0 1) (Set.Icc 0 1)) (hgc : ∀ u ∈ Set.Icc 0 1, ∀ z ∈ Set.Icc 0 1, T u ≤ z ↔ u ≤ F z) : ∫ (u : ℝ) in Set.Icc 0 1, |T u - u| = ∫ (z : ℝ) in Set.Icc 0 1, |F z - z|

The one-dimensional quantile/CDF identity, proved directly by expressing absolute displacement as an integral of threshold disagreements and swapping the two unit-interval integrals.

structure FD1D.MonotoneQuantilePolicy (F : ℝ → ℝ) : Type

An actual quantile map together with an actual selected point.

• monotoneCDF : MonotoneOn F (Set.Icc 0 1)
• cdf_measurable : Measurable F
• cdf_mapsTo : Set.MapsTo F (Set.Icc 0 1) (Set.Icc 0 1)
• quantileMap : ℝ → ℝ

  Measurable generalized inverse of the cumulative distribution function.

• quantile_measurable : Measurable self.quantileMap
• quantile_mapsTo : Set.MapsTo self.quantileMap (Set.Icc 0 1) (Set.Icc 0 1)
• generalizedInverse (u : ℝ) : u ∈ Set.Icc 0 1 → ∀ z ∈ Set.Icc 0 1, self.quantileMap u ≤ z ↔ u ≤ F z
• selectedPoint : ℝ → ℝ

  Measurable selected location approximating the quantile map.

• selected_measurable : Measurable self.selectedPoint
• selected_mapsTo : Set.MapsTo self.selectedPoint (Set.Icc 0 1) (Set.Icc 0 1)
• withinError : ℝ

  Uniform upper bound for the distance from a selected location to its quantile.

• withinError_nonneg : 0 ≤ self.withinError
• selected_close (u : ℝ) : u ∈ Set.Icc 0 1 → |self.selectedPoint u - self.quantileMap u| ≤ self.withinError

noncomputable def FD1D.MonotoneQuantilePolicy.expectedDistance {F : ℝ → ℝ} (P : MonotoneQuantilePolicy F) : ℝ

Actual cost of the selected-point policy against a uniform request.

Equations

• P.expectedDistance = ∫ (u : ℝ) in Set.Icc 0 1, |P.selectedPoint u - u|

noncomputable def FD1D.MonotoneQuantilePolicy.quantileDistance {F : ℝ → ℝ} (P : MonotoneQuantilePolicy F) : ℝ

Cost of the continuous generalized inverse before leaf rounding.

Equations

• P.quantileDistance = ∫ (u : ℝ) in Set.Icc 0 1, |P.quantileMap u - u|

theorem FD1D.MonotoneQuantilePolicy.quantileDistance_eq_cdfTransportArea {F : ℝ → ℝ} (P : MonotoneQuantilePolicy F) : P.quantileDistance = cdfTransportArea fun (z : ℝ) => F z - z

theorem FD1D.MonotoneQuantilePolicy.expectedDistance_le {F : ℝ → ℝ} (P : MonotoneQuantilePolicy F) : P.expectedDistance ≤ P.withinError + cdfTransportArea fun (z : ℝ) => F z - z

noncomputable def FD1D.DyadicMass.quantilePolicy {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : MonotoneQuantilePolicy q.piecewiseCDF

The explicit dyadic CDF, inverse, and leaf endpoint form an actual policy.

Equations

• One or more equations did not get rendered due to their size.

theorem FD1D.DyadicMass.exists_monotoneQuantilePolicy {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : ∃ (P : MonotoneQuantilePolicy q.piecewiseCDF), P.withinError = 1 / ↑(2 ^ L)

theorem FD1D.DyadicMass.quantile_cost_within_leaf {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : (q.quantilePolicy hq).expectedDistance ≤ 1 / ↑(2 ^ L) + cdfTransportArea fun (z : ℝ) => q.piecewiseCDF z - z

The actual selected-leaf endpoint has cost at most the exact quantile cost plus one depth-L cell width.

theorem FD1D.DyadicMass.quantile_discrepancy_eq_haar {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) {z : ℝ} (hz : z ∈ Set.Icc 0 1) : q.piecewiseCDF z - z = q.haarSeries z

For probability leaf masses, the CDF discrepancy used by the quantile policy is exactly the recursively defined integrated Haar series.

theorem FD1D.haarCombination_integrable {ι : Type u_1} [Fintype ι] (l p b : ι → ℝ) : MeasureTheory.Integrable (haarCombination l p b) MeasureTheory.volume

theorem FD1D.haarCombination_sq_integrable {ι : Type u_1} [Fintype ι] (l p b : ι → ℝ) (hp : ∀ (i : ι), 0 < p i) : MeasureTheory.Integrable (fun (z : ℝ) => haarCombination l p b z ^ 2) MeasureTheory.volume

theorem FD1D.cdfTransportArea_nonneg (f : ℝ → ℝ) : 0 ≤ cdfTransportArea f

theorem FD1D.integral_abs_sq_le_integral_sq {f : ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Icc 0 1) MeasureTheory.volume) (hfsq : MeasureTheory.IntegrableOn (fun (z : ℝ) => f z ^ 2) (Set.Icc 0 1) MeasureTheory.volume) : cdfTransportArea f ^ 2 ≤ ∫ (z : ℝ) in Set.Icc 0 1, f z ^ 2

Cauchy--Schwarz on the unit interval, proved by Jensen for x ↦ x².

theorem FD1D.cdfTransportArea_sq_le_haarL2 {ι : Type u_1} [Fintype ι] (l p b : ι → ℝ) (hp : ∀ (i : ι), 0 < p i) : cdfTransportArea (haarCombination l p b) ^ 2 ≤ haarL2 l p b

theorem FD1D.FiniteLaw.expect_sq_le_expect_sq {Ω : Type u_2} [Fintype Ω] (μ : FiniteLaw Ω) (f : Ω → ℝ) : μ.expect f ^ 2 ≤ μ.expect fun (ω : Ω) => f ω ^ 2

Weighted Cauchy--Schwarz for the project's finite-law expectation.

theorem FD1D.FiniteLaw.expect_le_sqrt_expect_sq {Ω : Type u_2} [Fintype Ω] (μ : FiniteLaw Ω) (f g : Ω → ℝ) (hf : ∀ (ω : Ω), 0 ≤ f ω) (hg : ∀ (ω : Ω), 0 ≤ g ω) (hfg : ∀ (ω : Ω), f ω ^ 2 ≤ g ω) : μ.expect f ≤ √(μ.expect g)

theorem FD1D.expected_area_le_sqrt_l2 {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [Fintype Ω] (μ : FiniteLaw Ω) (l p : ι → ℝ) (b : Ω → ι → ℝ) (hp : ∀ (i : ι), 0 < p i) : (μ.expect fun (ω : Ω) => cdfTransportArea (haarCombination l p (b ω))) ≤ √(μ.expect fun (ω : Ω) => haarL2 l p (b ω))

CDF-area transport followed by Cauchy--Schwarz in space and in state.

gap below is the abstract hazard telescope E[H_L] - m⁻². The hypothesis htelescope is equation (2): Σ p_v E[b_v²] ≤ 2 a² gap.

theorem FD1D.transport_cost_equation_three {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [Fintype Ω] (μ : FiniteLaw Ω) (l p : ι → ℝ) (b : Ω → ι → ℝ) (cost : Ω → ℝ) (n a gap : ℝ) (_hn : 0 < n) (ha : 0 ≤ a) (hgap : 0 ≤ gap) (hp : ∀ (i : ι), 0 < p i) (hcost : ∀ (ω : Ω), cost ω ≤ 1 / n + cdfTransportArea (haarCombination l p (b ω))) (hsym : ∀ (i j : ι), i ≠ j → IntervalsSeparated l p i j ∨ μ.OddSymmetry fun (ω : Ω) => b ω i * b ω j) (htelescope : (∑ i : ι, p i * μ.expect fun (ω : Ω) => b ω i ^ 2) ≤ 2 * a ^ 2 * gap) : μ.expect cost ≤ 1 / n + a / √6 * √gap

Equation (3), with the exact constant. hcost is the conditional monotone quantile bound plus the deterministic within-cell error 1/n.