Ancestry.lean`

63 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DiamondDistortion.intervalSystem line 14
Source documentation
A finite interval in an ancestral order. This keeps the root in every tree.
Also declared: ComparatorChallenges/DiamondDistortion.lean:207 (same declaration text).
```
def intervalSystem {ι : Type*} (r : ι → ι → Prop)
    (hrefl : ∀ a, r a a) (hanti : ∀ a b, r a b → r b a → a = b) : SegmentSystem ι where
…
```
Mentions: OAI.DiamondDistortion.SegmentSystem
class OAI.DiamondDistortion.Ancestry line 28
Source documentation
An ancestral partial order: the predecessors of any vertex form a chain.
Also declared: ComparatorChallenges/DiamondDistortion.lean:221 (same declaration text).
```
class Ancestry (ι : Type*) extends PartialOrder ι where
…
```
def OAI.DiamondDistortion.Ancestry.segments line 37
Source documentation
Nonempty finite intervals for an ancestral order.
Also declared: ComparatorChallenges/DiamondDistortion.lean:231 (same declaration text).
```
def segments : SegmentSystem ι :=
…
```
Mentions: OAI.DiamondDistortion.SegmentSystem
def OAI.DiamondDistortion.Ancestry.Ancestral line 41
Source documentation
Downward closed sets are precisely ancestral heads.
```
def Ancestral (H : Set ι) : Prop := ∀ ⦃a b : ι⦄, a ≤ b → b ∈ H → a ∈ H
```
lemma OAI.DiamondDistortion.Ancestry.ancestral_not_above line 43
lemma OAI.DiamondDistortion.Ancestry.interval_chain line 47
lemma OAI.DiamondDistortion.Ancestry.segment_filter_head line 53
lemma OAI.DiamondDistortion.Ancestry.segment_filter_tail line 76

lemma OAI.DiamondDistortion.Ancestry.split_energy_le line 102

Source documentation

Splitting each member of a disjoint family at its own ancestral cut preserves the testing budget. This is the simultaneous, not one-gate-at-a-time, estimate.

lemma split_energy_le (F : A.segments.Family) (H : Fin F.n → Set ι)
    (hH : ∀ i, A.Ancestral (H i)) (u : ι →₀ ℝ) :
    (∑ i, ((∑ v ∈ (F.seg i).filter (· ∈ H i), u v) ^ 2 +
      (∑ v ∈ (F.seg i).filter (· ∉ H i), u v) ^ 2)) ≤
      (A.segments.primalSeminorm u) ^ 2 := by
…

lemma OAI.DiamondDistortion.Ancestry.split_gain_le line 140

Source documentation

The explicit increase in the squared test after simultaneous splitting.

lemma split_gain_le (F : A.segments.Family) (H : Fin F.n → Set ι)
    (hH : ∀ i, A.Ancestral (H i)) (u : ι →₀ ℝ) :
    (∑ i, (∑ v ∈ F.seg i, u v) ^ 2) +
      2 * (∑ i : Fin F.n, ((∑ v ∈ (F.seg i).filter (· ∉ H i), u v) ^ 2 -
        (∑ v ∈ F.seg i, u v) * (∑ v ∈ (F.seg i).filter (· ∉ H i), u v))) ≤
        (A.segments.primalSeminorm u) ^ 2 := by
…

def OAI.DiamondDistortion.Ancestry.Gate line 163
Source documentation
A minimal vertex outside a head. Gates in a tree form an antichain.
```
def Gate (H : Set ι) (g : ι) : Prop :=
…
```
lemma OAI.DiamondDistortion.Ancestry.gates_eq_of_le line 166
lemma OAI.DiamondDistortion.Ancestry.gates_eq_of_common_upper line 171
lemma OAI.DiamondDistortion.Ancestry.gate_unique_in_segment line 177
lemma OAI.DiamondDistortion.Ancestry.exists_gate_le line 184
def OAI.DiamondDistortion.Ancestry.first line 202
Source documentation
Canonical lower endpoint; no ordering is imposed on segment families.
```
def first (F : A.segments.Family) (i : Fin F.n) : ι :=
…
```
lemma OAI.DiamondDistortion.Ancestry.first_spec line 205
lemma OAI.DiamondDistortion.Ancestry.first_le_of_mem line 209
lemma OAI.DiamondDistortion.Ancestry.first_mem line 214

lemma OAI.DiamondDistortion.Ancestry.crossing_cut_sum line 220

Source documentation

Two heads through a common exterior vertex are nested; cutting the longer at the shorter's first vertex preserves exactly the shorter head sum.

lemma crossing_cut_sum {H : Set ι} (hH : A.Ancestral H) (p : ι →₀ ℝ)
    (hp : ∀ v, v ∉ H → p v = 0) (F G : A.segments.Family)
    (i : Fin F.n) (j : Fin G.n) {g : ι} (hg : g ∉ H)
    (hgF : g ∈ F.seg i) (hgG : g ∈ G.seg j)
    (hfirst : A.first F i ≤ A.first G j) :
    (∑ v ∈ (F.seg i).filter (fun v => A.first G j ≤ v), p v) =
      ∑ v ∈ G.seg j, p v := by
…

lemma OAI.DiamondDistortion.Ancestry.sum_extend_zero line 255

Source documentation

Zero-extension along a finite injection preserves the finite sum.

lemma sum_extend_zero {κ ν : Type*} [Fintype κ] [Fintype ν]
    (e : κ ↪ ν) (f : κ → ℝ) :
    (∑ i, Function.extend e f (fun _ => 0) i) = ∑ a, f a := by
…

lemma OAI.DiamondDistortion.Ancestry.matched_split_gain_le line 271

Source documentation

Simultaneous splitting restricted to any injected list of original segments.

lemma matched_split_gain_le {κ : Type*} [Fintype κ]
    (F : A.segments.Family) (e : κ ↪ Fin F.n) (c : κ → ι) (p : ι →₀ ℝ) :
    (∑ i, (∑ v ∈ F.seg i, p v) ^ 2) +
      2 * (∑ a, ((∑ v ∈ (F.seg (e a)).filter (fun v => c a ≤ v), p v) ^ 2 -
        (∑ v ∈ F.seg (e a), p v) *
          (∑ v ∈ (F.seg (e a)).filter (fun v => c a ≤ v), p v))) ≤
      (A.segments.primalSeminorm p) ^ 2 := by
…

lemma OAI.DiamondDistortion.Ancestry.opposite_matching_le line 312

Source documentation

Opposite head sums, matched injectively in both families, spend only the combined testing deficits. This is the simultaneous boundary cancellation.

lemma opposite_matching_le {κ : Type*} [Fintype κ]
    {H : Set ι} (hH : A.Ancestral H) (p : ι →₀ ℝ)
    (hp : ∀ v, v ∉ H → p v = 0) (F G : A.segments.Family)
    (eF : κ ↪ Fin F.n) (eG : κ ↪ Fin G.n) (g : κ → ι)
    (hgH : ∀ a, g a ∉ H) (hgF : ∀ a, g a ∈ F.seg (eF a))
    (hgG : ∀ a, g a ∈ G.seg (eG a))
    (hopp : ∀ a, (∑ v ∈ F.seg (eF a), p v) * (∑ v ∈ G.seg (eG a), p v) < 0) :
    2 * (∑ a, |(∑ v ∈ F.seg (eF a), p v) * (∑ v ∈ G.seg (eG a), p v)|) ≤
      ((A.segments.primalSeminorm p) ^ 2 - ∑ i, (∑ v ∈ F.seg i, p v) ^ 2) +
      ((A.segments.primalSeminorm p) ^ 2 - ∑ j, (∑ v ∈ G.seg j, p v) ^ 2) := by
…

def OAI.DiamondDistortion.Ancestry.boundaryCoeff line 377
Source documentation
The (possibly zero) head sum carried by the unique segment at a gate.
```
def boundaryCoeff (F : A.segments.Family) (p : ι →₀ ℝ) (g : ι) : ℝ :=
…
```
lemma OAI.DiamondDistortion.Ancestry.boundaryCoeff_eq line 380
lemma OAI.DiamondDistortion.Ancestry.boundaryCoeff_nonzero_mem line 391

lemma OAI.DiamondDistortion.Ancestry.opposite_crossing_le line 400

Source documentation

Exact two-family opposite-crossing estimate, written without a sign-filter so that it can be averaged over independent finite endpoint laws.

lemma opposite_crossing_le {κ : Type*} [Fintype κ]
    {H : Set ι} (hH : A.Ancestral H) (p : ι →₀ ℝ)
    (hp : ∀ v, v ∉ H → p v = 0) (F G : A.segments.Family)
    (gate : κ ↪ ι) (hgate : ∀ a, A.Gate H (gate a)) :
    (∑ a, (|A.boundaryCoeff F p (gate a)| * |A.boundaryCoeff G p (gate a)| -
      A.boundaryCoeff F p (gate a) * A.boundaryCoeff G p (gate a))) ≤
      ((A.segments.primalSeminorm p) ^ 2 - ∑ i, (∑ v ∈ F.seg i, p v) ^ 2) +
      ((A.segments.primalSeminorm p) ^ 2 - ∑ j, (∑ v ∈ G.seg j, p v) ^ 2) := by
…

lemma OAI.DiamondDistortion.Ancestry.gate_coefficient_energy line 464
def OAI.DiamondDistortion.Ancestry.tailAt line 501
Source documentation
The tail from the unique segment through g, or the empty segment if absent.
```
def tailAt (F : A.segments.Family) (H : Finset ι) (g : ι) : Finset ι :=
…
```
lemma OAI.DiamondDistortion.Ancestry.tailAt_eq line 504
lemma OAI.DiamondDistortion.Ancestry.tailAt_mem line 515
lemma OAI.DiamondDistortion.Ancestry.tailAt_outside line 523
lemma OAI.DiamondDistortion.Ancestry.tailAt_allowed line 526
lemma OAI.DiamondDistortion.Ancestry.tailAt_cone line 539
lemma OAI.DiamondDistortion.Ancestry.tailAt_pairwise line 548
lemma OAI.DiamondDistortion.Ancestry.gate_on_nonzero_segment line 557
def OAI.DiamondDistortion.Ancestry.gateSet line 576
Source documentation
The represented finite set of all gates of H in K.
```
def gateSet (H K : Finset ι) : Finset ι := K.filter (A.Gate (H : Set ι))
```
lemma OAI.DiamondDistortion.Ancestry.mem_gateSet line 578

lemma OAI.DiamondDistortion.Ancestry.replaced_tail_eq line 583

Source documentation

Replacement coefficients have no wholly exterior contribution. Their entire tail is the sum of their crossing tails at the finitely represented gates.

lemma replaced_tail_eq {H K : Finset ι} (hH : A.Ancestral (H : Set ι))
    (hK : A.Ancestral (K : Set ι)) (F : A.segments.Family)
    (hFK : ∀ i, F.seg i ⊆ K) (p : ι →₀ ℝ) (hp : ∀ v, v ∉ H → p v = 0) :
    A.segments.tailDual H (A.segments.combine F.seg (fun i => ∑ v ∈ F.seg i, p v)) =
      A.segments.combine (fun g : A.gateSet H K => A.tailAt F H g.val)
        (fun g : A.gateSet H K => A.boundaryCoeff F p g.val) := by
…

lemma OAI.DiamondDistortion.Ancestry.primal_filter_le line 643
lemma OAI.DiamondDistortion.Ancestry.primal_filter_tail_le line 666

lemma OAI.DiamondDistortion.Ancestry.localize_family_energy line 691

Source documentation

Restricting any test family to a finite ancestral set gives one of the finitely many local families, with exactly the same energy for supported tests.

lemma localize_family_energy {K : Finset ι} (hK : A.Ancestral (K : Set ι))
    (F : A.segments.Family) (p : ι →₀ ℝ) (hp : ∀ v, v ∉ K → p v = 0) :
    ∃ G : A.segments.LocalFamily K,
      (∑ i, (∑ v ∈ F.seg i, p v) ^ 2) =
        ∑ S : A.segments.LocalIndex G, (∑ v ∈ S.val, p v) ^ 2 := by
…

lemma OAI.DiamondDistortion.Ancestry.primal_le_of_local_energies line 760

lemma OAI.DiamondDistortion.Ancestry.finite_atomic_representation line 779

Source documentation

Finite atomic-ball formula: exact inherited dual restrictions, derived by finite-dimensional separation rather than assumed as model data.

lemma finite_atomic_representation {K : Finset ι} (hK : A.Ancestral (K : Set ι))
    (x : A.segments.Dual) (hx : ‖x‖ ≤ 1) :
    ∃ c ∈ A.segments.coefficientBall K 1,
      A.segments.totalMap K c = fun v : K => x (A.segments.unitVector v.val) := by
…

lemma OAI.DiamondDistortion.Ancestry.finite_atomic_representation_radius line 825
lemma OAI.DiamondDistortion.Ancestry.headPrimal_norm_le line 851
lemma OAI.DiamondDistortion.Ancestry.tailPrimal_norm_le line 860
lemma OAI.DiamondDistortion.Ancestry.headDual_norm_le line 872
lemma OAI.DiamondDistortion.Ancestry.tailDual_norm_le line 880
lemma OAI.DiamondDistortion.Ancestry.replacement_error_le line 888
lemma OAI.DiamondDistortion.Ancestry.replacement_error_gate line 899
lemma OAI.DiamondDistortion.Ancestry.replacement_cross line 908
lemma OAI.DiamondDistortion.Ancestry.replacement_mass_norm line 919

lemma OAI.DiamondDistortion.Ancestry.pooled_tail_test line 949

Source documentation

The finite pooled coefficient/slack bound, before taking the supremum over head tests. No lens or convexity modulus is postulated for the space.

lemma pooled_tail_test {Ω : Type*} [Fintype Ω] {H K : Finset ι}
    (hH : A.Ancestral (H : Set ι)) (hK : A.Ancestral (K : Set ι))
    {R : ℝ} {x y : A.segments.Dual} (law : A.segments.BipolarLaw Ω R x y)
    (hFK : ∀ ω i,(law.atom ω).family.seg i ⊆ K)
    (hx : ∀ v,v ∉ H → x (A.segments.unitVector v)=0)
    (p : ι →₀ ℝ) (hp : ∀ v,v ∉ H → p v=0) (hpn : A.segments.primalSeminorm p ≤ 1) :
    ‖A.segments.tailDual H y‖ ≤
      2*Real.sqrt (R^2 - (x (A.segments.finiteEmbedding p))^2) := by
…

lemma OAI.DiamondDistortion.Ancestry.finite_lens_test line 1073

Source documentation

Pair the two exact finite atomic representations, retaining their common ancestral support and their actual endpoints.

lemma finite_lens_test {H K : Finset ι}
    (hH : A.Ancestral (H : Set ι)) (hK : A.Ancestral (K : Set ι)) (hHK : H ⊆ K)
    {R : ℝ} (hR : 0 < R) {x y : A.segments.Dual}
    (hx : ∀ v, v ∉ H → x (A.segments.unitVector v) = 0)
    (hplus : ‖x+y‖ ≤ R) (hminus : ‖x-y‖ ≤ R)
    (p : ι →₀ ℝ) (hp : ∀ v, v ∉ H → p v = 0) (hpn : A.segments.primalSeminorm p ≤ 1) :
    ‖A.segments.tailDual H (A.segments.headDual K y)‖ ≤
      2*Real.sqrt (R^2 - (x (A.segments.finiteEmbedding p))^2) := by
…

lemma OAI.DiamondDistortion.Ancestry.intrinsic_tail_test line 1101

Source documentation

Finite restrictions suffice for the full dual estimate: no shrinking or reflexivity hypothesis is needed for this intrinsic finite-head bound.

lemma intrinsic_tail_test
    (hfin : ∀ S : Finset ι, ∃ K : Finset ι, S ⊆ K ∧ A.Ancestral (K : Set ι))
    {H : Finset ι} (hH : A.Ancestral (H : Set ι)) {R : ℝ} (hR : 0 < R)
    {x y : A.segments.Dual} (hx : ∀ v, v ∉ H → x (A.segments.unitVector v) = 0)
    (hplus : ‖x+y‖ ≤ R) (hminus : ‖x-y‖ ≤ R)
    (p : ι →₀ ℝ) (hp : ∀ v, v ∉ H → p v = 0) (hpn : A.segments.primalSeminorm p ≤ 1) :
    ‖A.segments.tailDual H y‖ ≤
      2*Real.sqrt (R^2 - (x (A.segments.finiteEmbedding p))^2) := by
…

lemma OAI.DiamondDistortion.Ancestry.norm_center_le line 1126
lemma OAI.DiamondDistortion.Ancestry.intrinsic_tail_sq line 1134
lemma OAI.DiamondDistortion.Ancestry.finite_heads_of_predecessors line 1185
lemma OAI.DiamondDistortion.Ancestry.coordinate_predual_approximation line 1201

lemma OAI.DiamondDistortion.Ancestry.finite_head_pair line 1220

Source documentation

Finite-dimensional compactness compares distinct members of any bounded sequence; no maximum over the infinitely many children is asserted.

lemma finite_head_pair {H : Finset ι} (hH : A.Ancestral (H : Set ι))
    (z : ℕ → A.segments.Dual) {R η : ℝ} (hz : ∀ i, ‖z i‖ ≤ R) (hη : 0 < η) :
    ∃ i j : ℕ, i ≠ j ∧ ‖A.segments.headDual H ((1/2:ℝ) • (z i-z j))‖ < η := by
…

lemma OAI.DiamondDistortion.Ancestry.average_lens line 1249

lemma OAI.DiamondDistortion.Ancestry.separated_lens line 1266

Source documentation

Exact separated-lens consequence of the intrinsic estimate. Its only approximation input is explicitly proved for each target model below.

lemma separated_lens
    (hfin : ∀ S : Finset ι, ∃ K : Finset ι, S ⊆ K ∧ A.Ancestral (K : Set ι))
    {x : A.segments.Dual}
    (happrox : ∀ η > 0, ∃ H : Finset ι, A.Ancestral (H : Set ι) ∧ ‖A.segments.tailDual H x‖ < η)
    (z : ℕ → A.segments.Dual) {R ε : ℝ} (hR : 0 ≤ R) (hε : 0 < ε)
    (hplus : ∀ i, ‖x+z i‖ ≤ R) (hminus : ∀ i, ‖x-z i‖ ≤ R)
    (hsep : ∀ i j, i ≠ j → ε ≤ ‖z i-z j‖) :
    ‖x‖^2+ε^2/16 ≤ R^2 := by
…