Extracting a leaf with all remaining exact-image caps

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

proven

Loading review…

Natural Language Statement

Lemma

Among pin extensions that retain enough of the original mass, choose one of maximal rank. A remaining unusually likely positive-rank constraint would produce a larger candidate, so every such image test obeys the cap.

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

lem✓Lax342547.LeafExtraction

⊢Lax342547Proofs.LeafExtraction.exists_leaf

Lean source view on GitHub

Show types on hover

1	import Lax342547.ExactPins
2	import Mathlib.Probability.ProbabilityMassFunction.Constructions
3
4	/-!
5	---
6	title: Extracting a leaf with all remaining exact-image caps
7	type: lemma
8	---
9	Among pin extensions that retain enough of the original mass, choose one
10	of maximal rank. A remaining unusually likely positive-rank constraint
11	would produce a larger candidate, so every such image test obeys the cap.
12	-/
13
14	namespace Lax342547.LeafExtraction
15
16	open Lax342547.MomentSpace Lax342547.ExactPins
17	open scoped ENNReal
18
19	def Good {Ω Axis I N : Type} [Fintype Axis] (p : PMF Ω)
20	(A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
21	(P : Pin Axis I N) (S : Set Ω) (α : ℝ≥0∞) : Prop :=
22	∀ Q : Pin Axis I N, 1 ≤ P.relativeRank Q →
23	p.toOuterMeasure (S ∩ Q.event A) ≤ α ^ (P.relativeRank Q) * p.toOuterMeasure S
24
25	axiom exists_leaf {Ω Axis I N : Type}
26	[Fintype Axis] [Fintype I] [Fintype N]
27	(p : PMF Ω) (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
28	(P₀ : Pin Axis I N) (R : Set Ω) (hR : R ⊆ P₀.event A)
29	(δ α : ℝ≥0∞) (hα₀ : α ≠ 0) (hαtop : α ≠ ⊤) (hmass : δ < p.toOuterMeasure R) :
30	∃ P : Pin Axis I N, P₀.Extends P ∧
31	δ * α ^ (P.rank - P₀.rank) < p.toOuterMeasure (R ∩ P.event A) ∧
32	Good p A P (R ∩ P.event A) α
33
34	end Lax342547.LeafExtraction
35