Finite peeling into disjoint exact-pin leaves

Lax342547.LeafPartition · concepts/Lax342547/LeafPartition.lean · lax-342547

proven

Loading review…

Natural Language Statement

Lemma

Repeated leaf extraction partitions the retained support, leaving mass at most delta. Every leaf retains its original mass lower bound, exact pins, and all positive-rank relative image caps.

Concept map

4 concepts; 5 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

lem✓Lax342547.LeafPartition

⊢Lax342547Proofs.LeafPartition.exists_partition

Lean source view on GitHub

Show types on hover

1	import Lax342547.LeafExtraction
2	import Mathlib.Data.Finset.Union
3
4	/-!
5	---
6	title: Finite peeling into disjoint exact-pin leaves
7	type: lemma
8	---
9	Repeated leaf extraction partitions the retained support, leaving mass at
10	most delta. Every leaf retains its original mass lower bound, exact pins,
11	and all positive-rank relative image caps.
12	-/
13
14	namespace Lax342547.LeafPartition
15
16	open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.LeafExtraction
17	open scoped ENNReal
18
19	def Partition {Ω Axis I N : Type} [DecidableEq Ω] [Fintype Axis]
20	(p : PMF Ω) (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
21	(P₀ : Pin Axis I N) (R : Finset Ω) (δ α : ℝ≥0∞)
22	(L : Finset (Finset Ω × Pin Axis I N)) : Prop :=
23	(∀ z ∈ L, z.1 ⊆ R ∧ P₀.Extends z.2 ∧ (z.1 : Set Ω) ⊆ z.2.event A ∧
24	δ * α ^ (z.2.rank - P₀.rank) < p.toOuterMeasure z.1 ∧ Good p A z.2 z.1 α) ∧
25	(∀ z ∈ L, ∀ w ∈ L, z ≠ w → Disjoint z.1 w.1) ∧
26	p.toOuterMeasure (R \ L.biUnion Prod.fst : Finset Ω) ≤ δ
27
28	axiom exists_partition {Ω Axis I N : Type}
29	[DecidableEq Ω] [Fintype Axis] [Fintype I] [Fintype N]
30	(p : PMF Ω) (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
31	(P₀ : Pin Axis I N) (R : Finset Ω) (hR : (R : Set Ω) ⊆ P₀.event A)
32	(δ α : ℝ≥0∞) (hα₀ : α ≠ 0) (hαtop : α ≠ ⊤) :
33	∃ L : Finset (Finset Ω × Pin Axis I N), Partition p A P₀ R δ α L
34
35	end Lax342547.LeafPartition
36