Stat.Quantile.ConditionalMarkedSubsampleDkw
Boolean-marked subsample empirical-CDF concentration: exact mark-word conditioning, selected-coordinate iid laws, finite conditional aggregation, and DKW-style tail lifting.
Basic 12 core · 7 supporting This module defines exact mark words, their selected coordinates, and the empirical CDF obtained after retaining one Boolean arm. ★ selectedCDFBadEvent_inter_wordEvent
Boolean-marked finite samples
This module defines exact mark words, their selected coordinates, and the empirical CDF obtained after retaining one Boolean arm. The definitions are deterministic and form the reindexing layer for conditional probability arguments in the companion modules.
def selectedIndices reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a Boolean word and a requested mark, the selected positions are the finite set of coordinates carrying that mark, as given by filtering all coordinates.
def selectedWordCount reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a Boolean word and a requested mark, the selected count is the number of its selected positions, given by their cardinality.
Definition (Lean source)
def selectedIndex reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a Boolean word and a requested mark, the selected-coordinate embedding enumerates the selected positions in their original order, using the ordered finite-set enumeration.
Definition (Lean source)
def wordEvent reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a marked sample and a Boolean word, the exact-word event is the set of outcomes whose complete mark vector equals that word.
def selectedCount reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a marked sample, a requested mark, and a sample outcome, the selected count is the number of observed coordinates carrying that mark.
def selectedOutcomes reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a marked sample, a Boolean word, and a requested mark, the selected outcome vector takes the outcome component at each reindexed selected coordinate.
Definition (Lean source)
def empiricalCDFVec reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a finite real vector and a threshold, the vector empirical CDF is the normalized sum of lower-ray indicators. For the empty vector the normalizing inverse is zero by convention, so the value is zero.
def selectedEmpiricalCDF reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a marked sample, a requested mark, a sample outcome, and a threshold, the selected empirical CDF is the lower-ray count in the selected arm divided by its observed size. When the selected arm is empty the inverse size is zero by convention and the value is zero; the bad event below requires a nonempty arm.
def uniformCDFDeviation reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a measure on the real line and a finite real vector, the uniform empirical-CDF deviation is the supremum over thresholds of the absolute empirical-minus-population CDF difference. No probability assumption is made here; for a probability law, as assumed by the measurability and tail results, the differences are bounded and this is the usual uniform deviation, while an unbounded family has real supremum zero by convention.
Definition (Lean source)
parameters
def
uniformCDFDeviation ρ x :
ℝ
given by
def fixedCDFBadSet reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a measure on the real line (a population probability law in the results using it) and a deviation radius, the fixed-size bad set is the set of vectors whose uniform empirical-CDF deviation exceeds that radius.
Definition (Lean source)
parameters
given by
{x | uniformCDFDeviation ρ x > radius}
def selectedCDFBadEvent reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a marked sample, a requested mark, a measure on the real line (a population probability law in the results using it), and a count-indexed radius, the selected-sample bad event is the event that the selected arm is nonempty and its uniform deviation exceeds the radius at its observed size.
Definition (Lean source)
parameters
def
given by
{ω | selectedCount Z a ω > 0 ∧ sSup (Set.range fun y : ℝ => |selectedEmpiricalCDF Z a ω y - cdf ρ y|) > radius (selectedCount Z a ω)}
lemma selectedCDFBadEvent_inter_wordEvent reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
Given a marked sample, a requested mark, a population law, a count-indexed radius, a Boolean word, and a positive selected count for that word, intersecting the selected bad event with its exact-word event equals the reindexed fixed-size bad event intersected with that word event.
Formal statement
hypotheses
conclusion
selectedCDFBadEvent Z a ρ radius ∩ wordEvent Z w
Proof (Lean source)
lemma selectedCDFBadEvent_inter_wordEvent {Ω : Type*} {n : ℕ}
(Z : Fin n → Ω → Bool × ℝ) (a : Bool) (ρ : Measure ℝ)
(radius : ℕ → ℝ) (w : Fin n → Bool) (hw : 0 < selectedWordCount w a) :
selectedCDFBadEvent Z a ρ radius ∩ wordEvent Z w =
(selectedOutcomes Z w a) ⁻¹'
fixedCDFBadSet ρ (radius (selectedWordCount w a)) ∩ wordEvent Z w := by
-- Extensionality reduces this to the count identity and pointwise empirical-CDF reindexing.
ext ω
constructor
· rintro ⟨⟨_, hbad⟩, hω⟩
refine ⟨?_, hω⟩
simpa [fixedCDFBadSet, uniformCDFDeviation,
selectedCount_eq_on_wordEvent Z a w hω,
empiricalCDFVec_selectedOutcomes_eq Z a w hω] using hbad
· rintro ⟨hbad, hω⟩
refine ⟨⟨?_, ?_⟩, hω⟩
· simpa [selectedCount_eq_on_wordEvent Z a w hω] using hw
· simpa [fixedCDFBadSet, uniformCDFDeviation,
selectedCount_eq_on_wordEvent Z a w hω,
empiricalCDFVec_selectedOutcomes_eq Z a w hω] using hbad
7 supporting declarations (lemmas, instances)
-
selectedIndex_marklemma — For a Boolean word, a requested mark, and a selected-coordinate index, the coordinate selected by the embedding carries the requested mark.hypothesesconclusionw (selectedIndex w a j) = aProof (Lean source)
lemma selectedIndex_mark {n : ℕ} (w : Fin n → Bool) (a : Bool) (j : Fin (selectedWordCount w a)) : w (selectedIndex w a j) = a := by -- Unfold the filtered finset and use `Finset.orderEmbOfFin_mem`. classical have hj : selectedIndex w a j ∈ selectedIndices w a := by unfold selectedIndex apply Finset.orderEmbOfFin_mem exact (Finset.mem_filter.mp hj).2 -
sum_selectedIndexlemma — For a Boolean word, a requested mark, and a summand function, summing over the reindexed selected coordinates equals summing over all requested-mark positions.hypothesesconclusion= ∑ i ∈ selectedIndices w a, f iProof (Lean source)
lemma sum_selectedIndex {n : ℕ} (w : Fin n → Bool) (a : Bool) {R : Type*} [AddCommMonoid R] (f : Fin n → R) : (∑ j : Fin (selectedWordCount w a), f (selectedIndex w a j)) = ∑ i ∈ selectedIndices w a, f i := by -- Convert the left sum along `orderIsoOfFin`, then use `sum_subtype`. classical let hcard : (selectedIndices w a).card = selectedWordCount w a := rfl have hidx : selectedIndex w a = (selectedIndices w a).orderEmbOfFin hcard := rfl rw [hidx] calc (∑ j : Fin (selectedWordCount w a), f ((selectedIndices w a).orderEmbOfFin hcard j)) = ∑ i : ↥(selectedIndices w a), f i := by exact Equiv.sum_comp ((selectedIndices w a).orderIsoOfFin hcard).toEquiv (fun i : ↥(selectedIndices w a) => f i) _ = ∑ i ∈ selectedIndices w a, f i := Finset.sum_coe_sort _ _ -
measurableSet_wordEventlemma — Given a marked sample, measurability of every marked observation, and a Boolean word, the corresponding exact-word event is measurable.Proof (Lean source)
lemma measurableSet_wordEvent {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} (Z : Fin n → Ω → Bool × ℝ) (hZ : ∀ i, Measurable (Z i)) (w : Fin n → Bool) : MeasurableSet (wordEvent Z w) := by -- Express the event as a finite intersection of preimages of measurable Bool singletons. rw [show wordEvent Z w = ⋂ i, (fun ω => (Z i ω).1) ⁻¹' ({w i} : Set Bool) by ext ω simp [wordEvent]] exact MeasurableSet.iInter fun i => (measurableSet_singleton (w i)).preimage (hZ i).fst -
disjoint_wordEventlemma — Given a marked sample and two distinct Boolean words, their exact-word events are disjoint.hypothesesProof (Lean source)
lemma disjoint_wordEvent {Ω : Type*} {n : ℕ} (Z : Fin n → Ω → Bool × ℝ) {w v : Fin n → Bool} (hwv : w ≠ v) : Disjoint (wordEvent Z w) (wordEvent Z v) := by -- Choose a coordinate where the two words differ and contradict simultaneous membership. apply Set.disjoint_left.2 intro ω hωw hωv apply hwv funext i exact (hωw i).symm.trans (hωv i) -
iUnion_wordEventlemma — For a marked sample, the union of all exact-word events is the whole sample space.hypotheses -
selectedCount_eq_on_wordEventlemma — Given a marked sample, a requested mark, a Boolean word, and an outcome in that word's event, the observed selected count equals the word's deterministic selected count.hypothesesconclusionselectedCount Z a ω = selectedWordCount w aProof (Lean source)
lemma selectedCount_eq_on_wordEvent {Ω : Type*} {n : ℕ} (Z : Fin n → Ω → Bool × ℝ) (a : Bool) (w : Fin n → Bool) {ω : Ω} (hω : ω ∈ wordEvent Z w) : selectedCount Z a ω = selectedWordCount w a := by -- Membership in `wordEvent` identifies the two filtered finsets extensionally. classical unfold selectedCount selectedWordCount selectedIndices congr 1 ext i simp only [mem_filter, Finset.mem_univ, true_and] rw [hω i] -
empiricalCDFVec_selectedOutcomes_eqlemma — Given a marked sample, a requested mark, a Boolean word, an outcome in its exact-word event, and a threshold, the reindexed-vector empirical CDF equals the directly selected empirical CDF.Proof (Lean source)
lemma empiricalCDFVec_selectedOutcomes_eq {Ω : Type*} {n : ℕ} (Z : Fin n → Ω → Bool × ℝ) (a : Bool) (w : Fin n → Bool) {ω : Ω} (hω : ω ∈ wordEvent Z w) (y : ℝ) : empiricalCDFVec (selectedOutcomes Z w a ω) y = selectedEmpiricalCDF Z a ω y := by -- Rewrite the count on the word event and apply `sum_selectedIndex`. classical have hs : Finset.univ.filter (fun i => (Z i ω).1 = a) = selectedIndices w a := by ext i simp [selectedIndices, hω i] simp only [empiricalCDFVec, selectedOutcomes, selectedEmpiricalCDF] rw [selectedCount_eq_on_wordEvent Z a w hω, hs] congr 1 exact sum_selectedIndex w a (fun i => cdfStat y (Z i ω).2)
ConditionalLaw 3 core · 6 supporting This module conditions a finite i.i.d. ★ selectedOutcomes_conditionalLaw
Conditional law of a Boolean-marked subsample
This module conditions a finite i.i.d. family of marked real observations on its complete Boolean word. It proves that the coordinates selected by a fixed mark, reindexed in their original order, have the expected finite product law.
structure MarkedIID reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
A finite marked iid experiment packages the marked observation family, its coordinatewise measurability, mutual independence, and the common marginal law.
Definition (Lean source)
parameters
fields
structure BooleanMarkFactorization reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
A Boolean mark factorization packages a positive requested-mark mass and the identity expressing each marked outcome-set mass as that mass times the outcome law.
theorem selectedOutcomes_conditionalLaw reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw.MarkedIID
Given a finite marked iid experiment, a requested mark, its mass, a selected-outcome law, a Boolean mark factorization, a Boolean word, and positive probability for that word, the reindexed selected outcome vector conditioned on the word has the finite iid product law with marginal ρ.
Formal statement
hypotheses
Ω :
Type*
n :
ℕ
μ :
Measure Ω
S :
MarkedIID Ω n μ ν
a :
e :
ℝ≥0∞
ρ :
hfac :
BooleanMarkFactorization ν a e ρ
hw :
μ (wordEvent S.Z w) ≠ 0
conclusion
Measure.map (selectedOutcomes S.Z w a) μ[|wordEvent S.Z w]
= Measure.pi (fun _ : Fin (selectedWordCount w a) => ρ)
Proof (Lean source)
theorem MarkedIID.selectedOutcomes_conditionalLaw {Ω : Type*} [MeasurableSpace Ω]
{n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)}
[IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
(S : MarkedIID Ω n μ ν) (a : Bool) (e : ℝ≥0∞) (ρ : Measure ℝ)
[IsProbabilityMeasure ρ] (hfac : BooleanMarkFactorization ν a e ρ)
(w : Fin n → Bool) (hw : μ (wordEvent S.Z w) ≠ 0) :
Measure.map (selectedOutcomes S.Z w a) μ[|wordEvent S.Z w] =
Measure.pi (fun _ : Fin (selectedWordCount w a) => ρ) := by
-- Use `iIndepFun.map_fun_eq_pi_map` and rewrite every marginal with the preceding lemma.
calc
Measure.map (selectedOutcomes S.Z w a) μ[|wordEvent S.Z w] =
Measure.pi (fun j =>
Measure.map (fun ω => selectedOutcomes S.Z w a ω j) μ[|wordEvent S.Z w]) := by
exact iIndepFun.map_fun_eq_pi_map
(fun j => (S.measurable (selectedIndex w a j)).snd.aemeasurable)
(S.selectedOutcomes_iIndep_cond_word a w hw)
_ = Measure.pi (fun _ : Fin (selectedWordCount w a) => ρ) := by
congr 1
funext j
exact S.selectedOutcome_map_cond_word_eq a e ρ hfac w hw j
6 supporting declarations (lemmas, instances)
-
measure_wordEvent_eq_prodlemma — Given a finite marked iid experiment and a Boolean word, the probability of its exact-word event equals the product of its coordinatewise mark probabilities.hypothesesconclusionμ (wordEvent S.Z w) = ∏ i, ν {z | z.1 = w i}Proof (Lean source)
lemma MarkedIID.measure_wordEvent_eq_prod {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} (S : MarkedIID Ω n μ ν) (w : Fin n → Bool) : μ (wordEvent S.Z w) = ∏ i, ν {z | z.1 = w i} := by -- Apply the finite-intersection characterization of `iIndepFun`, then each marginal map law. rw [show wordEvent S.Z w = ⋂ i, S.Z i ⁻¹' {z | z.1 = w i} by ext ω simp [wordEvent]] rw [S.indep.meas_iInter] · apply Finset.prod_congr rfl intro i _ calc μ (S.Z i ⁻¹' {z | z.1 = w i}) = μ.map (S.Z i) {z | z.1 = w i} := (Measure.map_apply (S.measurable i) ((measurableSet_singleton (w i)).preimage measurable_fst)).symm _ = ν {z | z.1 = w i} := by rw [S.law i] · intro i exact ⟨{z | z.1 = w i}, (measurableSet_singleton (w i)).preimage measurable_fst, rfl⟩ -
map_snd_cond_mark_eqlemma — Given a finite marked iid experiment, a requested mark, its mass, a probability law for selected outcomes, a Boolean mark factorization, and a coordinate, conditioning that coordinate's outcome on its requested mark gives the selected-outcome law.hypothesesΩ :Type*n :ℕμ :Measure ΩS :MarkedIID Ω n μ νa :e :ℝ≥0∞ρ :hfac :BooleanMarkFactorization ν a e ρi :Fin nconclusionMeasure.map (fun ω => (S.Z i ω).2) μ[|{ω | (S.Z i ω).1 = a}] = ρProof (Lean source)
lemma MarkedIID.map_snd_cond_mark_eq {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (S : MarkedIID Ω n μ ν) (a : Bool) (e : ℝ≥0∞) (ρ : Measure ℝ) [IsProbabilityMeasure ρ] (hfac : BooleanMarkFactorization ν a e ρ) (i : Fin n) : Measure.map (fun ω => (S.Z i ω).2) μ[|{ω | (S.Z i ω).1 = a}] = ρ := by -- Use `Measure.ext`; `cond_apply` turns each measurable test set into the factorization ratio. have hmark_meas : MeasurableSet {ω | (S.Z i ω).1 = a} := (measurableSet_singleton a).preimage (S.measurable i).fst have hνmark : ν {z | z.1 = a} = e := by simpa using hfac.joint Set.univ MeasurableSet.univ have hμmark : μ {ω | (S.Z i ω).1 = a} = e := by calc μ {ω | (S.Z i ω).1 = a} = μ.map (S.Z i) {z | z.1 = a} := (Measure.map_apply (S.measurable i) ((measurableSet_singleton a).preimage measurable_fst)).symm _ = ν {z | z.1 = a} := by rw [S.law i] _ = e := hνmark have he_top : e ≠ ∞ := by rw [← hνmark] exact measure_ne_top ν _ ext B hB rw [Measure.map_apply (S.measurable i).snd hB, cond_apply hmark_meas, hμmark] have hjoint : μ ({ω | (S.Z i ω).1 = a} ∩ (fun ω => (S.Z i ω).2) ⁻¹' B) = e * ρ B := by calc μ ({ω | (S.Z i ω).1 = a} ∩ (fun ω => (S.Z i ω).2) ⁻¹' B) = μ (S.Z i ⁻¹' {z | z.1 = a ∧ z.2 ∈ B}) := by congr 1 _ = μ.map (S.Z i) {z | z.1 = a ∧ z.2 ∈ B} := (Measure.map_apply (S.measurable i) (((measurableSet_singleton a).preimage measurable_fst).inter (hB.preimage measurable_snd))).symm _ = ν {z | z.1 = a ∧ z.2 ∈ B} := by rw [S.law i] _ = e * ρ B := hfac.joint B hB rw [hjoint, ← mul_assoc, ENNReal.inv_mul_cancel hfac.positive he_top, one_mul] -
outcomes_iIndep_cond_wordlemma — Given a finite marked iid experiment, a Boolean word, and positive probability for its exact-word event, all outcome coordinates remain mutually independent after conditioning on that event.hypothesesconclusioniIndepFun (fun i ω => (S.Z i ω).2) μ[|wordEvent S.Z w]Proof (Lean source)
lemma MarkedIID.outcomes_iIndep_cond_word {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} [IsProbabilityMeasure μ] (S : MarkedIID Ω n μ ν) (w : Fin n → Bool) (hw : μ (wordEvent S.Z w) ≠ 0) : iIndepFun (fun i ω => (S.Z i ω).2) μ[|wordEvent S.Z w] := by -- Swap each pair, invoke `iIndepFun.cond`, and derive nonzero coordinate mark events from `hw`. have hprod : ∏ i, ν {z | z.1 = w i} ≠ 0 := by rw [← S.measure_wordEvent_eq_prod w] exact hw have hνmark (i : Fin n) : ν {z | z.1 = w i} ≠ 0 := (Finset.prod_ne_zero_iff.mp hprod) i (Finset.mem_univ i) have hμmark (i : Fin n) : μ ((fun ω => (S.Z i ω).1) ⁻¹' {w i}) ≠ 0 := by calc μ ((fun ω => (S.Z i ω).1) ⁻¹' {w i}) = μ.map (S.Z i) {z | z.1 = w i} := (Measure.map_apply (S.measurable i) ((measurableSet_singleton (w i)).preimage measurable_fst)).symm _ = ν {z | z.1 = w i} := by rw [S.law i] _ ≠ 0 := hνmark i have hindep : iIndepFun (fun i ω => ((S.Z i ω).2, (S.Z i ω).1)) μ := by simpa [Function.comp_def] using S.indep.comp (fun (_ : Fin n) => fun z : Bool × ℝ => (z.2, z.1)) (fun _ => measurable_snd.prodMk measurable_fst) have hcond := iIndepFun.cond (X := fun i ω => (S.Z i ω).2) (Y := fun i ω => (S.Z i ω).1) (t := fun i => {w i}) (fun i => (S.measurable i).fst) hindep hμmark (fun i => measurableSet_singleton (w i)) have hevent : (⋂ i, (fun ω => (S.Z i ω).1) ⁻¹' {w i}) = wordEvent S.Z w := by ext ω simp [wordEvent] rw [hevent] at hcond exact hcond -
selectedOutcome_map_cond_word_eqlemma — Given a finite marked iid experiment, a requested mark, its mass, a selected-outcome law, a Boolean mark factorization, a Boolean word, positive probability for that word, and a selected-coordinate index, that reindexed selected outcome has law ρ after conditioning on the complete word.hypothesesΩ :Type*n :ℕμ :Measure ΩS :MarkedIID Ω n μ νa :e :ℝ≥0∞ρ :hfac :BooleanMarkFactorization ν a e ρhw :μ (wordEvent S.Z w) ≠ 0j :Fin (selectedWordCount w a)conclusionMeasure.map (fun ω => selectedOutcomes S.Z w a ω j) μ[|wordEvent S.Z w] = ρProof (Lean source)
lemma MarkedIID.selectedOutcome_map_cond_word_eq {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (S : MarkedIID Ω n μ ν) (a : Bool) (e : ℝ≥0∞) (ρ : Measure ℝ) [IsProbabilityMeasure ρ] (hfac : BooleanMarkFactorization ν a e ρ) (w : Fin n → Bool) (hw : μ (wordEvent S.Z w) ≠ 0) (j : Fin (selectedWordCount w a)) : Measure.map (fun ω => selectedOutcomes S.Z w a ω j) μ[|wordEvent S.Z w] = ρ := by -- `cond_iInter` shows that conditioning on the other marks does not change this marginal. let k : Fin n := selectedIndex w a j have hk : w k = a := selectedIndex_mark w a j have hprod : ∏ i, ν {z | z.1 = w i} ≠ 0 := by rw [← S.measure_wordEvent_eq_prod w] exact hw have hνmark (i : Fin n) : ν {z | z.1 = w i} ≠ 0 := (Finset.prod_ne_zero_iff.mp hprod) i (Finset.mem_univ i) have hμmark (i : Fin n) : μ ((fun ω => (S.Z i ω).1) ⁻¹' {w i}) ≠ 0 := by calc μ ((fun ω => (S.Z i ω).1) ⁻¹' {w i}) = μ.map (S.Z i) {z | z.1 = w i} := (Measure.map_apply (S.measurable i) ((measurableSet_singleton (w i)).preimage measurable_fst)).symm _ = ν {z | z.1 = w i} := by rw [S.law i] _ ≠ 0 := hνmark i have hindep : iIndepFun (fun i ω => ((S.Z i ω).2, (S.Z i ω).1)) μ := by simpa [Function.comp_def] using S.indep.comp (fun (_ : Fin n) => fun z : Bool × ℝ => (z.2, z.1)) (fun _ => measurable_snd.prodMk measurable_fst) have hevent : (⋂ i, (fun ω => (S.Z i ω).1) ⁻¹' {w i}) = wordEvent S.Z w := by ext ω simp [wordEvent] ext B hB change (Measure.map (fun ω => (S.Z k ω).2) μ[|wordEvent S.Z w]) B = ρ B rw [Measure.map_apply ((S.measurable k).snd) hB] change μ[(fun ω => (S.Z k ω).2) ⁻¹' B | wordEvent S.Z w] = ρ B rw [← hevent] have hcond := cond_iInter (X := fun i ω => (S.Z i ω).2) (Y := fun i ω => (S.Z i ω).1) (f := fun i => (fun ω => (S.Z i ω).2) ⁻¹' B) (t := fun i => {w i}) (s := {k}) (fun i => (S.measurable i).fst) hindep (fun i _ => ⟨B, hB, rfl⟩) (fun i _ => hμmark i) (fun i => measurableSet_singleton (w i)) have hsingle : μ[(fun ω => (S.Z k ω).2) ⁻¹' B | ⋂ i, (fun ω => (S.Z i ω).1) ⁻¹' {w i}] = μ[(fun ω => (S.Z k ω).2) ⁻¹' B | (fun ω => (S.Z k ω).1) ⁻¹' {w k}] := by simpa using hcond rw [hsingle] have hmarg := congrArg (fun m : Measure ℝ => m B) (S.map_snd_cond_mark_eq a e ρ hfac k) rw [Measure.map_apply (S.measurable k).snd hB] at hmarg rw [hk] have hmarkset : (fun ω => (S.Z k ω).1) ⁻¹' {a} = {ω | (S.Z k ω).1 = a} := by ext ω simp rw [hmarkset] exact hmarg -
selectedOutcomes_iIndep_cond_wordlemma — Given a finite marked iid experiment, a requested mark, a Boolean word, and positive probability for its exact-word event, the reindexed selected outcomes remain mutually independent after conditioning on that event.hypothesesconclusioniIndepFun (fun j ω => selectedOutcomes S.Z w a ω j) μ[|wordEvent S.Z w]Proof (Lean source)
lemma MarkedIID.selectedOutcomes_iIndep_cond_word {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} [IsProbabilityMeasure μ] (S : MarkedIID Ω n μ ν) (a : Bool) (w : Fin n → Bool) (hw : μ (wordEvent S.Z w) ≠ 0) : iIndepFun (fun j ω => selectedOutcomes S.Z w a ω j) μ[|wordEvent S.Z w] := by -- Precompose `outcomes_iIndep_cond_word` with the injective selected-coordinate embedding. simpa [selectedOutcomes] using iIndepFun.precomp (selectedIndex w a).injective (S.outcomes_iIndep_cond_word w hw) -
measurable_selectedOutcomeslemma — Given a finite marked iid experiment, a requested mark, and a Boolean word, the map from a sample outcome to its reindexed selected outcome vector is measurable.hypothesesconclusionMeasurable (selectedOutcomes S.Z w a)Proof (Lean source)
lemma measurable_selectedOutcomes {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} (S : MarkedIID Ω n μ ν) (a : Bool) (w : Fin n → Bool) : Measurable (selectedOutcomes S.Z w a) := by -- Apply `measurable_pi_lambda`; each coordinate is a projection of `S.measurable`. exact measurable_pi_lambda _ fun j => (S.measurable (selectedIndex w a j)).snd
Measurability 1 core · 2 supporting This module supplies the separability step needed to treat the supremum over all real thresholds as an ordinary measurable random variable. ★ measurableSet_fixedCDFBadSet
Measurability of finite empirical-CDF deviations
This module supplies the separability step needed to treat the supremum over all real thresholds as an ordinary measurable random variable. In particular, callers of the tail-lifting theorem do not need to assume an extra measurability side condition beyond the fixed-size probability bound.
lemma measurableSet_fixedCDFBadSet reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a probability law and a deviation radius, the fixed-size uniform empirical-CDF bad set is measurable.
Formal statement
hypotheses
conclusion
MeasurableSet (fixedCDFBadSet (m := m) ρ radius)
Proof (Lean source)
lemma measurableSet_fixedCDFBadSet {m : ℕ} (ρ : Measure ℝ)
[IsProbabilityMeasure ρ] (radius : ℝ) :
MeasurableSet (fixedCDFBadSet (m := m) ρ radius) := by
-- This is the measurable preimage of the open upper ray `(radius, ∞)`.
change MeasurableSet ((uniformCDFDeviation (m := m) ρ) ⁻¹' Ioi radius)
exact measurableSet_Ioi.preimage (measurable_uniformCDFDeviation ρ)
2 supporting declarations (lemmas, instances)
-
empiricalCDFVec_continuousWithinAt_Icilemma — For a finite real vector and a threshold, its empirical CDF is continuous from the right at that threshold.Proof (Lean source)
lemma empiricalCDFVec_continuousWithinAt_Ici {m : ℕ} (x : Fin m → ℝ) (y : ℝ) : ContinuousWithinAt (empiricalCDFVec x) (Ici y) y := by classical have hstat (i : Fin m) : ContinuousWithinAt (fun t : ℝ => cdfStat t (x i)) (Ici y) y := by by_cases hxy : x i ≤ y · have hc : ContinuousWithinAt (fun _ : ℝ => (1 : ℝ)) (Ici y) y := continuousWithinAt_const refine hc.congr ?_ ?_ · intro z hz simp [cdfStat, hxy.trans hz] · simp [cdfStat, hxy] · have hyx : y < x i := lt_of_not_ge hxy have hc : ContinuousWithinAt (fun _ : ℝ => (0 : ℝ)) (Ici y) y := continuousWithinAt_const refine hc.congr_of_eventuallyEq ?_ ?_ · filter_upwards [Filter.Eventually.filter_mono inf_le_left (Iio_mem_nhds hyx)] with z hz simp [cdfStat, not_le.mpr hz] · simp [cdfStat, hxy] have hsum : ContinuousWithinAt (fun t : ℝ => ∑ i : Fin m, cdfStat t (x i)) (Ici y) y := by let s : Finset (Fin m) := univ change ContinuousWithinAt (fun t : ℝ => ∑ i ∈ s, cdfStat t (x i)) (Ici y) y induction s using Finset.induction_on with | empty => simpa using (continuousWithinAt_const : ContinuousWithinAt (fun _ : ℝ => (0 : ℝ)) (Ici y) y) | @insert a s ha ih => simp only [Finset.sum_insert, ha, not_false_eq_true] exact (hstat a).add ih change ContinuousWithinAt (fun t : ℝ => (m : ℝ)⁻¹ * ∑ i : Fin m, cdfStat t (x i)) (Ici y) y exact hsum.const_mul (m : ℝ)⁻¹ -
measurable_uniformCDFDeviationlemma — For a probability law, the uniform empirical-CDF deviation of a finite real vector from that law is measurable.Proof (Lean source)
lemma measurable_uniformCDFDeviation {m : ℕ} (ρ : Measure ℝ) [IsProbabilityMeasure ρ] : Measurable (uniformCDFDeviation (m := m) ρ) := by -- Reduce the real supremum to a countable dense family of thresholds using right continuity. have hpoint (y : ℝ) : Measurable (fun x : Fin m → ℝ => |empiricalCDFVec x y - cdf ρ y|) := by apply Measurable.abs apply Measurable.sub · unfold empiricalCDFVec fun_prop · fun_prop have hbound (x : Fin m → ℝ) (y : ℝ) : |empiricalCDFVec x y - cdf ρ y| ≤ 1 := by have hstat_nonneg : 0 ≤ ∑ i : Fin m, cdfStat y (x i) := sum_nonneg fun i _ => cdfStat_nonneg y (x i) have hstat_le : (∑ i : Fin m, cdfStat y (x i)) ≤ m := by calc (∑ i : Fin m, cdfStat y (x i)) ≤ ∑ _i : Fin m, (1 : ℝ) := Finset.sum_le_sum fun i _ => cdfStat_le_one y (x i) _ = m := by simp have he0 : 0 ≤ empiricalCDFVec x y := by simp only [empiricalCDFVec] positivity have he1 : empiricalCDFVec x y ≤ 1 := by by_cases hm : m = 0 · subst m simp [empiricalCDFVec] · rw [empiricalCDFVec, inv_mul_le_iff₀ (by positivity)] simpa using hstat_le have hc0 := cdf_nonneg ρ y have hc1 := cdf_le_one ρ y rw [abs_le] constructor <;> linarith have hsep (x : Fin m → ℝ) : uniformCDFDeviation ρ x = ⨆ q : ℚ, |empiricalCDFVec x (q : ℝ) - cdf ρ (q : ℝ)| := by let g : ℝ → ℝ := fun y => |empiricalCDFVec x y - cdf ρ y| have hg_bound (y : ℝ) : g y ≤ 1 := hbound x y have hreal_bdd : BddAbove (range g) := by refine ⟨1, ?_⟩ rintro _ ⟨y, rfl⟩ exact hg_bound y have hrat_bdd : BddAbove (range fun q : ℚ => g (q : ℝ)) := by refine ⟨1, ?_⟩ rintro _ ⟨q, rfl⟩ exact hg_bound q change sSup (range g) = ⨆ q : ℚ, g (q : ℝ) apply le_antisymm · apply csSup_le · exact ⟨g 0, ⟨0, rfl⟩⟩ · intro z hz rcases hz with ⟨y, rfl⟩ obtain ⟨u, _, hu_above, hu_lim⟩ := Rat.denseRange_cast.exists_seq_strictAnti_tendsto Rat.cast_strictMono.monotone y have hdev : ContinuousWithinAt g (Ici y) y := ((empiricalCDFVec_continuousWithinAt_Ici x y).sub ((cdf ρ).right_continuous y)).abs have hu_within : Tendsto (cast ∘ u) atTop (𝓝[Ici y] y) := tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hu_lim (Filter.Eventually.of_forall fun n => Set.mem_Ici.mpr (le_of_lt (Set.mem_Ioi.mp (hu_above n)))) apply le_of_tendsto' (hdev.tendsto.comp hu_within) intro n exact le_ciSup hrat_bdd (u n) · apply ciSup_le intro q exact le_csSup hreal_bdd ⟨(q : ℝ), rfl⟩ rw [show uniformCDFDeviation (m := m) ρ = fun x => ⨆ q : ℚ, |empiricalCDFVec x (q : ℝ) - cdf ρ (q : ℝ)| from funext hsep] exact Measurable.iSup fun q => hpoint q
TailLift 2 core · 2 supporting This module lifts any fixed-size i.i.d. ★ conditionalMarkedSubsample_empiricalCDF_tail
Empirical-CDF tail bounds after Boolean selection
This module lifts any fixed-size i.i.d. empirical-CDF tail bound through independent Boolean marking and the resulting random sample size. It also packages the count-dependent radius used with the sharp two-sided DKW--Massart bound.
theorem conditionalMarkedSubsample_empiricalCDF_tail reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
Given a finite marked iid experiment, a requested mark, its mass, a selected-outcome law, a Boolean mark factorization, a count-indexed radius, a probability bound, and the corresponding fixed-size iid empirical-CDF bound at every positive sample size, the probability that the selected arm is nonempty and its uniform empirical-CDF deviation exceeds its count-indexed radius is at most β.
Formal statement
hypotheses
Ω :
Type*
n :
ℕ
μ :
Measure Ω
S :
MarkedIID Ω n μ ν
a :
e :
ℝ≥0∞
ρ :
hfac :
BooleanMarkFactorization ν a e ρ
radius :
ℕ → ℝ
β :
ℝ≥0∞
hfixed :
∀ m : ℕ
if
0 < m
then
(Measure.pi (fun _ : Fin m => ρ)) (fixedCDFBadSet ρ (radius m)) ≤ β
conclusion
μ (selectedCDFBadEvent S.Z a ρ radius) ≤ β
Proof (Lean source)
theorem conditionalMarkedSubsample_empiricalCDF_tail
{Ω : Type*} [MeasurableSpace Ω] {n : ℕ}
{μ : Measure Ω} {ν : Measure (Bool × ℝ)}
[IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
(S : MarkedIID Ω n μ ν) (a : Bool) (e : ℝ≥0∞) (ρ : Measure ℝ)
[IsProbabilityMeasure ρ] (hfac : BooleanMarkFactorization ν a e ρ)
(radius : ℕ → ℝ) (β : ℝ≥0∞)
(hfixed : ∀ m : ℕ, 0 < m →
(Measure.pi (fun _ : Fin m => ρ)) (fixedCDFBadSet ρ (radius m)) ≤ β) :
μ (selectedCDFBadEvent S.Z a ρ radius) ≤ β := by
-- Apply finite aggregation to exact words; positive-count cells use the conditional product law.
-- Rewrite the cell intersection with `selectedCDFBadEvent_inter_wordEvent`, turn its pullback
-- probability into a mapped conditional measure via `Measure.map_apply`, and then rewrite that
-- map with `selectedOutcomes_conditionalLaw`. Zero-count cells again have empty intersection.
apply measure_le_of_cond_le_on_finite_partition μ
(fun w : Fin n → Bool => wordEvent S.Z w)
(fun w => measurableSet_wordEvent S.Z S.measurable w)
(fun w v hwv => disjoint_wordEvent S.Z hwv)
(iUnion_wordEvent S.Z) (selectedCDFBadEvent S.Z a ρ radius)
(measurableSet_selectedCDFBadEvent S a ρ radius) β
intro w hwprob
by_cases hw : 0 < selectedWordCount w a
· rw [cond_apply (measurableSet_wordEvent S.Z S.measurable w),
inter_comm (wordEvent S.Z w),
selectedCDFBadEvent_inter_wordEvent S.Z a ρ radius w hw]
calc
(μ (wordEvent S.Z w))⁻¹ *
μ ((selectedOutcomes S.Z w a) ⁻¹'
fixedCDFBadSet ρ (radius (selectedWordCount w a)) ∩ wordEvent S.Z w) =
(Measure.map (selectedOutcomes S.Z w a) μ[|wordEvent S.Z w])
(fixedCDFBadSet ρ (radius (selectedWordCount w a))) := by
rw [Measure.map_apply (measurable_selectedOutcomes S a w)
(measurableSet_fixedCDFBadSet ρ _),
cond_apply (measurableSet_wordEvent S.Z S.measurable w), inter_comm]
_ = (Measure.pi (fun _ : Fin (selectedWordCount w a) => ρ))
(fixedCDFBadSet ρ (radius (selectedWordCount w a))) := by
rw [S.selectedOutcomes_conditionalLaw a e ρ hfac w hwprob]
_ ≤ β := hfixed (selectedWordCount w a) hw
· rw [cond_apply (measurableSet_wordEvent S.Z S.measurable w)]
have hinter : wordEvent S.Z w ∩ selectedCDFBadEvent S.Z a ρ radius = ∅ := by
ext ω
constructor
· rintro ⟨hword, hbad⟩
exact (hw (by simpa [selectedCount_eq_on_wordEvent S.Z a w hword] using hbad.1)).elim
· simp
simp [hinter]
def dkwRadius reviewed
⚑ flagged
Causalean.Stat.Quantile.ConditionalMarkedSubsampleDkw
For a confidence parameter and a selected count, the DKW confidence radius is the square root of log(4/α) divided by twice that count. It is a DKW radius for a confidence parameter that is positive and at most one and a positive count, as assumed by the tail theorems; outside that domain the logarithm, division and square-root conventions give values without that meaning (for example zero at count zero).
2 supporting declarations (lemmas, instances)
-
measurableSet_selectedCDFBadEventlemma — Given a finite marked iid experiment, a requested mark, a selected-outcome probability law, and a count-indexed radius, the selected-subsample empirical-CDF bad event is measurable.hypothesesconclusionMeasurableSet (selectedCDFBadEvent S.Z a ρ radius)Proof (Lean source)
lemma measurableSet_selectedCDFBadEvent {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} (S : MarkedIID Ω n μ ν) (a : Bool) (ρ : Measure ℝ) [IsProbabilityMeasure ρ] (radius : ℕ → ℝ) : MeasurableSet (selectedCDFBadEvent S.Z a ρ radius) := by -- Decompose over words and use `measurableSet_fixedCDFBadSet` on positive-count pullbacks. -- For a zero-count word, `selectedCount_eq_on_wordEvent` makes the intersection empty. rw [show selectedCDFBadEvent S.Z a ρ radius = ⋃ w : Fin n → Bool, selectedCDFBadEvent S.Z a ρ radius ∩ wordEvent S.Z w by ext ω constructor · intro hbad have hcover : ω ∈ ⋃ w : Fin n → Bool, wordEvent S.Z w := by rw [iUnion_wordEvent] exact Set.mem_univ ω rcases Set.mem_iUnion.mp hcover with ⟨w, hword⟩ exact Set.mem_iUnion_of_mem w ⟨hbad, hword⟩ · rintro h rcases Set.mem_iUnion.mp h with ⟨w, hbad, _⟩ exact hbad] exact MeasurableSet.iUnion fun w => by by_cases hw : 0 < selectedWordCount w a · rw [selectedCDFBadEvent_inter_wordEvent S.Z a ρ radius w hw] exact ((measurableSet_fixedCDFBadSet ρ _).preimage (measurable_selectedOutcomes S a w)).inter (measurableSet_wordEvent S.Z S.measurable w) · rw [show selectedCDFBadEvent S.Z a ρ radius ∩ wordEvent S.Z w = ∅ by ext ω constructor · rintro ⟨hbad, hword⟩ exact (hw (by simpa [selectedCount_eq_on_wordEvent S.Z a w hword] using hbad.1)).elim · simp] exact MeasurableSet.empty -
conditionalMarkedSubsample_dkwRadiustheorem — Given a finite marked iid experiment, a requested mark, its mass, a selected-outcome law, a Boolean mark factorization, a confidence parameter between zero and one, and the fixed-size DKW--Massart bound at every positive sample size, the selected-subsample empirical-CDF deviation at the DKW radius has tail probability at most α/2.hypothesesΩ :Type*n :ℕμ :Measure ΩS :MarkedIID Ω n μ νa :e :ℝ≥0∞ρ :hfac :BooleanMarkFactorization ν a e ρα :ℝhα :0 < αhα_one :α ≤ 1hDKW :∀ m : ℕif0 < mthen≤ ofReal (α / 2)conclusionProof (Lean source)
theorem conditionalMarkedSubsample_dkwRadius {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} {μ : Measure Ω} {ν : Measure (Bool × ℝ)} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (S : MarkedIID Ω n μ ν) (a : Bool) (e : ℝ≥0∞) (ρ : Measure ℝ) [IsProbabilityMeasure ρ] (hfac : BooleanMarkFactorization ν a e ρ) (α : ℝ) (hα : 0 < α) (hα_one : α ≤ 1) (hDKW : ∀ m : ℕ, 0 < m → (Measure.pi (fun _ : Fin m => ρ)) (fixedCDFBadSet ρ (dkwRadius α m)) ≤ ofReal (α / 2)) : μ (selectedCDFBadEvent S.Z a ρ (dkwRadius α)) ≤ ofReal (α / 2) := by -- This is the generic lifting theorem specialized to `dkwRadius` and the supplied DKW bound. exact conditionalMarkedSubsample_empiricalCDF_tail S a e ρ hfac (dkwRadius α) (ofReal (α / 2)) hDKW