Stat.Concentration.Poisson.EmpiricalRadius
These bounds use the count-dependent radius H * (sqrt ((w/m) * δ) + δ).
EmpiricalRadius 3 core · 2 supporting These bounds use the count-dependent radius H * (sqrt ((w/m) * δ) + δ). ★ poisson_empiricalRadius_bad_probability★ poisson_empiricalRadius_bad_fourth_moment
Empirical Poisson radii and bad-event moments
These bounds use the count-dependent radius H * (sqrt ((w/m) * δ) + δ).
The established self-normalized Poisson estimates provide exponential bad-event
probabilities and second/fourth moment envelopes, including zero intensity.
def empiricalRadius reviewed
⚑ flagged
Causalean.Stat.Concentration.Poisson
The empirical Poisson radius with multiplier H, exposure m, level δ, and observed count w is H times the sum of √((w/m)·δ) and δ.
Definition (Lean source)
parameters
H :
ℝ
m :
ℝ≥0
δ :
ℝ
w :
ℕ
def
empiricalRadius H m δ w :
ℝ
given by
H * (sqrt (((w : ℝ) / (m : ℝ)) * δ) + δ)
theorem poisson_empiricalRadius_bad_probability reviewed
⚑ flagged
Causalean.Stat.Concentration.Poisson
For a Poisson count with mean m·q, built from a nonnegative intensity q and exposure m, where the exposure is positive, the radius multiplier H is at least the universal constant 1024, and the level L is at least 1, the probability that the normalized deviation |w/m − q| exceeds a quarter of the empirical radius at level L/m is at most 2·exp(−40 L).
Formal statement
hypotheses
conclusion
poissonMeasure (m * q) {w : ℕ | normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4}
Proof (Lean source)
-- Rewrite the normalized deviation and radius with the private algebra in
-- `SelfNormalized.Scaling`; on `H ≥ universalH`, include this bad event in
-- `badEvent universalH L (m*q)` and apply `poisson_badEvent_probability`.
theorem poisson_empiricalRadius_bad_probability
(q m : ℝ≥0) (hm : 0 < m) (H L : ℝ) (hH : universalH ≤ H)
(hL : 1 ≤ L) :
poissonMeasure (m * q)
{w : ℕ | normalizedDeviation m q w >
empiricalRadius H m (L / (m : ℝ)) w / 4} ≤
ofReal (2 * exp (-40 * L)) := by
calc
_ ≤ poissonMeasure (m * q) (badEvent universalH L (m * q)) :=
measure_mono (empirical_bad_subset q m hm H L hH hL)
_ ≤ 2 * ofReal (exp (-(scalarDecay * L))) :=
poisson_badEvent_probability (m * q) hL
_ = ofReal (2 * exp (-40 * L)) := by
rw [show scalarDecay = (40 : ℝ) by rfl,
ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 2)]
norm_num
theorem poisson_empiricalRadius_bad_fourth_moment reviewed
⚑ flagged
Causalean.Stat.Concentration.Poisson
For a Poisson count with mean m·q, built from a nonnegative intensity q and exposure m, where the exposure is positive, the radius multiplier H is at least the universal constant 1024, and the level L is at least 1, the expected fourth-power failure score — the fourth power of the normalized deviation plus the empirical radius at level L/m, taken on the event that the deviation exceeds a quarter of that radius and zero otherwise — is at most (H/1024)^4 times the order-4 bad-moment constant times exp(−20 L) times (√(qL/m) + L/m)^4.
Formal statement
hypotheses
conclusion
∫ w : ℕ, (if normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4 then (normalizedDeviation m q w + empiricalRadius H m (L / (m : ℝ)) w) ^ 4 else 0) ∂poissonMeasure (m * q)
≤ (H / universalH) ^ 4 * scalarBadMomentConstant 4 * exp (-20 * L) * (sqrt ((q : ℝ) * L / (m : ℝ)) + L / (m : ℝ)) ^ 4
Proof (Lean source)
-- Same comparison as the second moment, using the existing scalar theorem at
-- `t=4`; its `exp (-40L)` decay is stronger than the displayed `exp (-20L)`.
theorem poisson_empiricalRadius_bad_fourth_moment
(q m : ℝ≥0) (hm : 0 < m) (H L : ℝ)
(hH : universalH ≤ H) (hL : 1 ≤ L) :
∫ w : ℕ,
(if normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4
then (normalizedDeviation m q w + empiricalRadius H m (L / (m : ℝ)) w) ^ 4
else 0) ∂poissonMeasure (m * q) ≤
(H / universalH) ^ 4 * scalarBadMomentConstant 4 *
exp (-20 * L) *
(sqrt ((q : ℝ) * L / (m : ℝ)) + L / (m : ℝ)) ^ 4 := by
exact empirical_bad_moment q m hm H L hH hL (inr (inr rfl))
2 supporting declarations (lemmas, instances)
-
empiricalRadius_eq_normalizedRadiustheorem — The empirical radius with multiplier H at level L/m equals H times the normalized radius at level numerator L, for every nonnegative exposure m and count w.hypothesesH L :ℝm :ℝ≥0w :ℕconclusionempiricalRadius H m (L / (m : ℝ)) w = H * normalizedRadius m L wProof (Lean source)
theorem empiricalRadius_eq_normalizedRadius (H L : ℝ) (m : ℝ≥0) (w : ℕ) : empiricalRadius H m (L / (m : ℝ)) w = H * normalizedRadius m L w := by rfl -
poisson_empiricalRadius_bad_second_momenttheorem — For a Poisson count with mean m·q, built from a nonnegative intensity q and exposure m, where the exposure is positive, the radius multiplier H is at least the universal constant 1024, and the level L is at least 1, the expected squared failure score — the square of the normalized deviation plus the empirical radius at level L/m, taken on the event that the deviation exceeds a quarter of that radius and zero otherwise — is at most (H/1024)^2 times the order-2 bad-moment constant times exp(−20 L) times (√(qL/m) + L/m)^2.hypothesesconclusion∫ w : ℕ, (if normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4 then (normalizedDeviation m q w + empiricalRadius H m (L / (m : ℝ)) w) ^ 2 else 0) ∂poissonMeasure (m * q)≤ (H / universalH) ^ 2 * scalarBadMomentConstant 2 * exp (-20 * L) * (sqrt ((q : ℝ) * L / (m : ℝ)) + L / (m : ℝ)) ^ 2Proof (Lean source)
-- On the larger universal bad event, compare the H-score to -- `(H/universalH) * score universalH`; then apply -- `poisson_weighted_bad_moment` at `t=2` and divide by `m^2`. theorem poisson_empiricalRadius_bad_second_moment (q m : ℝ≥0) (hm : 0 < m) (H L : ℝ) (hH : universalH ≤ H) (hL : 1 ≤ L) : ∫ w : ℕ, (if normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4 then (normalizedDeviation m q w + empiricalRadius H m (L / (m : ℝ)) w) ^ 2 else 0) ∂poissonMeasure (m * q) ≤ (H / universalH) ^ 2 * scalarBadMomentConstant 2 * exp (-20 * L) * (sqrt ((q : ℝ) * L / (m : ℝ)) + L / (m : ℝ)) ^ 2 := by exact empirical_bad_moment q m hm H L hH hL (inr (inl rfl))
Product 3 core · 6 supporting This module compares count-dependent empirical Poisson radii with self-normalized raw scores and transfers the finite independent-product bad-event moment bound to four coordinates. ★ independent_poisson_empiricalRadius_badAny_moment_four
Product empirical-radius Poisson moments
This module compares count-dependent empirical Poisson radii with self-normalized raw scores and transfers the finite independent-product bad-event moment bound to four coordinates.
def empiricalBadAny reviewed
⚑ flagged
Causalean.Stat.Concentration.Poisson.EmpiricalRadius
For finite count coordinates, an exposure and intensities, and a multiplier and level, the empirical bad union contains precisely the outcomes where some normalized deviation exceeds one quarter of its empirical radius.
Definition (Lean source)
parameters
def
given by
{ω | ∃ i, normalizedDeviation m (q i) (W i ω) > empiricalRadius H m (L / (m : ℝ)) (W i ω) / 4}
def empiricalAggregateScore reviewed
⚑ flagged
Causalean.Stat.Concentration.Poisson.EmpiricalRadius
For finite count coordinates, an exposure and intensities, a multiplier and level, and an outcome, the empirical aggregate score sums each coordinate's normalized deviation and count-dependent radius.
Definition (Lean source)
parameters
def
empiricalAggregateScore W H L m q ω :
ℝ
given by
∑ i, (normalizedDeviation m (q i) (W i ω) + empiricalRadius H m (L / (m : ℝ)) (W i ω))
theorem independent_poisson_empiricalRadius_badAny_moment_four reviewed
⚑ flagged
Causalean.Stat.Concentration.Poisson.EmpiricalRadius
Under a probability law, four measurable Poisson counts with intensities and positive exposure and mutual independence, for moment order one, two, or four and a multiplier and level above their universal thresholds, H at least 1024 and L at least 1, the expectation of the t-th power of the empirical aggregate score, taken on the event that some coordinate's normalized deviation exceeds a quarter of its empirical radius and zero otherwise, is at most (H/1024)^t times the four-coordinate order-t product moment constant times exp(−20 L) times (√((sum of the four intensities) · L/m) + L/m)^t. Each count has Poisson mean equal to the exposure times its intensity.
Formal statement
hypotheses
Ω :
Type*
μ :
W :
Fin 4 → Ω → ℕ
q :
Fin 4 → ℝ≥0
m :
ℝ≥0
hm :
0 < m
hWmeas :
∀ i, Measurable (W i)
hWlaw :
∀ i, HasLaw (W i) (poissonMeasure (m * q i)) μ
hWindep :
iIndepFun W μ
t :
ℕ
ht :
t = 1 ∨ t = 2 ∨ t = 4
H L :
ℝ
hH :
universalH ≤ H
hL :
1 ≤ L
conclusion
∫ ω, (empiricalBadAny W H L m q).indicator (fun ω => (empiricalAggregateScore W H L m q ω) ^ t) ω ∂μ
≤ (H / universalH) ^ t * productMomentConstant 4 t * exp (-20 * L) * (sqrt ((∑ i, (q i : ℝ)) * L / (m : ℝ)) + L / (m : ℝ)) ^ t
Proof (Lean source)
-- Apply empiricalBadAny_subset_raw and empiricalAggregateScore_le_raw
-- pointwise. Use the integrability of the universal raw indicator score
-- (from the product theorem's supporting lemmas), integral_mono_of_nonneg,
-- and independent_poisson_badAny_moment_four; pull out
-- (H/universalH)^t/m^t and use empiricalRadius_totalLocalScale_div.
theorem independent_poisson_empiricalRadius_badAny_moment_four
{Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsProbabilityMeasure μ]
(W : Fin 4 → Ω → ℕ) (q : Fin 4 → ℝ≥0) (m : ℝ≥0) (hm : 0 < m)
(hWmeas : ∀ i, Measurable (W i))
(hWlaw : ∀ i, HasLaw (W i) (poissonMeasure (m * q i)) μ)
(hWindep : iIndepFun W μ)
{t : ℕ} (ht : t = 1 ∨ t = 2 ∨ t = 4)
(H L : ℝ) (hH : universalH ≤ H) (hL : 1 ≤ L) :
∫ ω, (empiricalBadAny W H L m q).indicator
(fun ω => (empiricalAggregateScore W H L m q ω) ^ t) ω ∂μ ≤
(H / universalH) ^ t * productMomentConstant 4 t * exp (-20 * L) *
(sqrt ((∑ i, (q i : ℝ)) * L / (m : ℝ)) + L / (m : ℝ)) ^ t := by
classical
let lambda : Fin 4 → ℝ≥0 := fun i => m * q i
let c : ℝ := H / universalH
have hc : 0 ≤ c := by
dsimp [c]
exact div_nonneg (le_trans universalH_pos.le hH) universalH_pos.le
have hmR : 0 < (m : ℝ) := NNReal.coe_pos.mpr hm
have hscoreInt (i : Fin 4) :
Integrable (fun ω => (score universalH L (lambda i) (W i ω)) ^ t) μ := by
have h := integrable_score_pow (lambda i) hL (t := t)
have hmap : μ.map (W i) = poissonMeasure (lambda i) := (hWlaw i).map_eq
rw [← hmap] at h
exact h.comp_aemeasurable (hWlaw i).aemeasurable
have hdomInt : Integrable
(fun ω => (4 : ℝ) ^ (t - 1) *
∑ i, (score universalH L (lambda i) (W i ω)) ^ t) μ := by
exact (integrable_finsetSum _ fun i _ => hscoreInt i).const_mul _
have hscore0 (i : Fin 4) (ω : Ω) :
0 ≤ score universalH L (lambda i) (W i ω) := by
unfold score deviation radius
exact add_nonneg (abs_nonneg _) (mul_nonneg universalH_pos.le (by positivity))
have hraw0 (ω : Ω) : 0 ≤
(badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω := by
by_cases hb : ω ∈ badAny W universalH L lambda
· rw [Set.indicator_of_mem hb]
apply pow_nonneg
unfold aggregateScore
exact Finset.sum_nonneg fun i _ => hscore0 i ω
· simp [hb]
have hrawDom (ω : Ω) :
(badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ≤
(4 : ℝ) ^ (t - 1) *
∑ i, (score universalH L (lambda i) (W i ω)) ^ t := by
have hpow : (aggregateScore W universalH L lambda ω) ^ t ≤
(4 : ℝ) ^ (t - 1) *
∑ i, (score universalH L (lambda i) (W i ω)) ^ t := by
unfold aggregateScore
rcases ht with rfl | rfl | rfl
· simp
· simpa using (pow_sum_le_card_mul_sum_pow
(s := (Finset.univ : Finset (Fin 4)))
(f := fun i => score universalH L (lambda i) (W i ω))
(fun i _ => hscore0 i ω) 1)
· simpa using (pow_sum_le_card_mul_sum_pow
(s := (Finset.univ : Finset (Fin 4)))
(f := fun i => score universalH L (lambda i) (W i ω))
(fun i _ => hscore0 i ω) 3)
by_cases hb : ω ∈ badAny W universalH L lambda
· simpa [hb] using hpow
· rw [Set.indicator_of_notMem hb]
exact mul_nonneg (pow_nonneg (by norm_num) _) (Finset.sum_nonneg fun i _ =>
pow_nonneg (hscore0 i ω) _)
have hrawMeas : Measurable
(fun ω => (badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω) := by
unfold badAny aggregateScore score deviation radius
measurability
have hrawInt : Integrable
(fun ω => (badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω) μ := by
exact integrable_of_le_of_le hrawMeas.aestronglyMeasurable
(Filter.Eventually.of_forall fun ω => hraw0 ω)
(Filter.Eventually.of_forall fun ω => hrawDom ω)
(integrable_zero _ _ _) hdomInt
have hemp0 (ω : Ω) : 0 ≤ empiricalAggregateScore W H L m q ω := by
unfold empiricalAggregateScore
apply Finset.sum_nonneg
intro i _
have hd : 0 ≤ normalizedDeviation m (q i) (W i ω) := by
unfold normalizedDeviation
positivity
have hr : 0 ≤ empiricalRadius H m (L / (m : ℝ)) (W i ω) := by
rw [empiricalRadius_eq_normalizedRadius]
unfold normalizedRadius
have hH0 : 0 ≤ H := le_trans universalH_pos.le hH
positivity
positivity
have hpoint (ω : Ω) :
(empiricalBadAny W H L m q).indicator
(fun ω => (empiricalAggregateScore W H L m q ω) ^ t) ω ≤
(c / (m : ℝ)) ^ t * (badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω := by
by_cases hb : ω ∈ empiricalBadAny W H L m q
· have hrb : ω ∈ badAny W universalH L lambda :=
empiricalBadAny_subset_raw W q m hm H L hH hL hb
simp only [Set.indicator_of_mem hb, Set.indicator_of_mem hrb]
calc
(empiricalAggregateScore W H L m q ω) ^ t ≤
(c * (aggregateScore W universalH L lambda ω / (m : ℝ))) ^ t :=
pow_le_pow_left₀ (hemp0 ω)
(empiricalAggregateScore_le_raw W q m hm H L hH hL ω) t
_ = (c / (m : ℝ)) ^ t * (aggregateScore W universalH L lambda ω) ^ t := by
have heq : c * (aggregateScore W universalH L lambda ω / (m : ℝ)) =
(c / (m : ℝ)) * aggregateScore W universalH L lambda ω := by ring
rw [heq, mul_pow]
· rw [Set.indicator_of_notMem hb]
exact mul_nonneg (pow_nonneg (div_nonneg hc hmR.le) _) (hraw0 ω)
have hempIndicator0 : 0 ≤ᵐ[μ] fun ω =>
(empiricalBadAny W H L m q).indicator
(fun ω => (empiricalAggregateScore W H L m q ω) ^ t) ω := by
filter_upwards [] with ω
by_cases hb : ω ∈ empiricalBadAny W H L m q
· rw [Set.indicator_of_mem hb]
exact pow_nonneg (hemp0 ω) _
· simp [hb]
have hmono :
∫ ω, (empiricalBadAny W H L m q).indicator
(fun ω => (empiricalAggregateScore W H L m q ω) ^ t) ω ∂μ ≤
(c / (m : ℝ)) ^ t *
∫ ω, (badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ := by
calc
_ ≤ ∫ ω, (c / (m : ℝ)) ^ t *
(badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ := by
apply integral_mono_of_nonneg hempIndicator0
(hrawInt.const_mul _)
exact Filter.Eventually.of_forall hpoint
_ = _ := integral_const_mul _ _
have hprod := independent_poisson_badAny_moment_four μ W lambda hWmeas
(by simpa [lambda] using hWlaw) hWindep ht hL
have hscale :
(sqrt ((∑ i, (lambda i : ℝ)) * L) + L) / (m : ℝ) =
sqrt ((∑ i, (q i : ℝ)) * L / (m : ℝ)) + L / (m : ℝ) := by
change localScale (∑ i, m * q i) L / (m : ℝ) = _
exact empiricalRadius_totalLocalScale_div q m hm L hL
calc
∫ ω, (empiricalBadAny W H L m q).indicator
(fun ω => (empiricalAggregateScore W H L m q ω) ^ t) ω ∂μ ≤
(c / (m : ℝ)) ^ t *
∫ ω, (badAny W universalH L lambda).indicator
(fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ := hmono
_ ≤ (c / (m : ℝ)) ^ t *
(productMomentConstant 4 t * exp (-20 * L) *
(sqrt ((∑ i, (lambda i : ℝ)) * L) + L) ^ t) := by
exact mul_le_mul_of_nonneg_left hprod
(pow_nonneg (div_nonneg hc hmR.le) _)
_ = (H / universalH) ^ t * productMomentConstant 4 t * exp (-20 * L) *
(sqrt ((∑ i, (q i : ℝ)) * L / (m : ℝ)) + L / (m : ℝ)) ^ t := by
rw [← hscale]
dsimp [c]
simp only [div_pow]
ring
6 supporting declarations (lemmas, instances)
-
empiricalRadius_bad_subset_rawtheorem — For a positive exposure, an intensity, a multiplier and level with the standard lower bounds, every empirical-radius bad count belongs to the universal raw-score bad event.hypothesesconclusion{w : ℕ | normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4} ⊆ badEvent universalH L (m * q)Proof (Lean source)
-- Rewrite normalized deviation and empirical radius as the corresponding raw -- quantities divided by m; compare thresholds using H ≥ universalH. theorem empiricalRadius_bad_subset_raw (q m : ℝ≥0) (hm : 0 < m) (H L : ℝ) (hH : universalH ≤ H) (hL : 1 ≤ L) : {w : ℕ | normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4} ⊆ badEvent universalH L (m * q) := by intro w hw have hmR : 0 < (m : ℝ) := NNReal.coe_pos.mpr hm have hr : 0 ≤ radius L w := by unfold radius positivity change normalizedDeviation m q w > empiricalRadius H m (L / (m : ℝ)) w / 4 at hw rw [scalar_normalizedDeviation_eq_div m q hm, empiricalRadius_eq_normalizedRadius, scalar_normalizedRadius_eq_div m hm] at hw change deviation (m * q) w > (universalH / 4) * radius L w have hthreshold : (universalH / 4) * radius L w ≤ H * (radius L w / (m : ℝ)) / 4 * (m : ℝ) := by rw [show H * (radius L w / (m : ℝ)) / 4 * (m : ℝ) = (H / 4) * radius L w by field_simp] exact mul_le_mul_of_nonneg_right (by linarith : universalH / 4 ≤ H / 4) hr have := (lt_div_iff₀ hmR).mp hw exact lt_of_le_of_lt hthreshold this -
empiricalRadius_score_le_rawtheorem — For a positive exposure, an intensity, a multiplier and level with the standard lower bounds, each empirical deviation-plus-radius score is at most the scaled universal raw score.hypothesesconclusionnormalizedDeviation m q w + empiricalRadius H m (L / (m : ℝ)) w≤ (H / universalH) * (score universalH L (m * q) w / (m : ℝ))Proof (Lean source)
-- Use the same normalized/raw identities as the subset lemma, then the -- nonnegativity of the raw deviation and H/universalH ≥ 1. theorem empiricalRadius_score_le_raw (q m : ℝ≥0) (hm : 0 < m) (H L : ℝ) (hH : universalH ≤ H) (hL : 1 ≤ L) (w : ℕ) : normalizedDeviation m q w + empiricalRadius H m (L / (m : ℝ)) w ≤ (H / universalH) * (score universalH L (m * q) w / (m : ℝ)) := by have hmR : 0 < (m : ℝ) := NNReal.coe_pos.mpr hm have hu : 0 < universalH := universalH_pos have hd : 0 ≤ deviation (m * q) w := by simp [deviation] have hr : 0 ≤ radius L w := by unfold radius; positivity rw [scalar_normalizedDeviation_eq_div m q hm, empiricalRadius_eq_normalizedRadius, scalar_normalizedRadius_eq_div m hm] unfold score have hc : 1 ≤ H / universalH := (le_div_iff₀ hu).2 (by simpa using hH) have hdev : deviation (m * q) w ≤ (H / universalH) * deviation (m * q) w := by nlinarith [mul_nonneg (sub_nonneg.mpr hc) hd] have hid : (H / universalH) * (deviation (m * q) w + universalH * radius L w) = (H / universalH) * deviation (m * q) w + H * radius L w := by field_simp calc deviation (m * q) w / (m : ℝ) + H * (radius L w / (m : ℝ)) = (deviation (m * q) w + H * radius L w) / (m : ℝ) := by ring _ ≤ ((H / universalH) * (deviation (m * q) w + universalH * radius L w)) / (m : ℝ) := by apply (div_le_div_iff_of_pos_right hmR).2 rw [hid] linarith _ = _ := by ring -
empiricalRadius_localScale_divtheorem — For an intensity and positive exposure and a level of at least one, the raw local scale divided by exposure equals the normalized local scale.hypothesesq m :ℝ≥0hm :0 < mL :ℝhL :1 ≤ LconclusionlocalScale (m * q) L / (m : ℝ) = sqrt ((q : ℝ) * L / (m : ℝ)) + L / (m : ℝ)Proof (Lean source)
-- Rewrite sqrt ((m*q)*L)/m using sqrt_div and sqrt (m²) = m. theorem empiricalRadius_localScale_div (q m : ℝ≥0) (hm : 0 < m) (L : ℝ) (hL : 1 ≤ L) : localScale (m * q) L / (m : ℝ) = sqrt ((q : ℝ) * L / (m : ℝ)) + L / (m : ℝ) := by have hmR : 0 < (m : ℝ) := NNReal.coe_pos.mpr hm have hsqrt : sqrt (((m : ℝ) * (q : ℝ)) * L) / (m : ℝ) = sqrt (((q : ℝ) * L) / (m : ℝ)) := by symm calc sqrt (((q : ℝ) * L) / (m : ℝ)) = sqrt ((((m : ℝ) * (q : ℝ)) * L) / ((m : ℝ) ^ 2)) := by congr 1 field_simp _ = sqrt (((m : ℝ) * (q : ℝ)) * L) / sqrt ((m : ℝ) ^ 2) := by rw [Real.sqrt_div] positivity _ = sqrt (((m : ℝ) * (q : ℝ)) * L) / (m : ℝ) := by rw [Real.sqrt_sq_eq_abs, abs_of_pos hmR] unfold localScale rw [NNReal.coe_mul, add_div, hsqrt] -
empiricalBadAny_subset_rawtheorem — For finite count coordinates, positive exposure, intensities, and a multiplier and level with their lower bounds, the empirical bad union is contained in the universal raw-score bad union.hypothesesι Ω :Type*Fintype ιW :ι → Ω → ℕq :ι → ℝ≥0m :ℝ≥0hm :0 < mH L :ℝhH :universalH ≤ HhL :1 ≤ LconclusionProof (Lean source)
-- Unpack the witnessing coordinate and apply empiricalRadius_bad_subset_raw. theorem empiricalBadAny_subset_raw {ι Ω : Type*} [Fintype ι] (W : ι → Ω → ℕ) (q : ι → ℝ≥0) (m : ℝ≥0) (hm : 0 < m) (H L : ℝ) (hH : universalH ≤ H) (hL : 1 ≤ L) : empiricalBadAny W H L m q ⊆ badAny W universalH L (fun i => m * q i) := by intro ω hω obtain ⟨i, hi⟩ := hω exact ⟨i, empiricalRadius_bad_subset_raw (q i) m hm H L hH hL hi⟩ -
empiricalAggregateScore_le_rawtheorem — For finite count coordinates, positive exposure, intensities, and a multiplier and level with their lower bounds, the empirical aggregate score is bounded by the scaled universal raw aggregate score at every outcome.hypothesesι Ω :Type*Fintype ιW :ι → Ω → ℕq :ι → ℝ≥0m :ℝ≥0hm :0 < mH L :ℝhH :universalH ≤ HhL :1 ≤ Lω :ΩconclusionempiricalAggregateScore W H L m q ωProof (Lean source)
-- Sum empiricalRadius_score_le_raw over coordinates and use Finset.sum_div. theorem empiricalAggregateScore_le_raw {ι Ω : Type*} [Fintype ι] (W : ι → Ω → ℕ) (q : ι → ℝ≥0) (m : ℝ≥0) (hm : 0 < m) (H L : ℝ) (hH : universalH ≤ H) (hL : 1 ≤ L) (ω : Ω) : empiricalAggregateScore W H L m q ω ≤ (H / universalH) * (aggregateScore W universalH L (fun i => m * q i) ω / (m : ℝ)) := by unfold empiricalAggregateScore aggregateScore calc (∑ i, (normalizedDeviation m (q i) (W i ω) + empiricalRadius H m (L / (m : ℝ)) (W i ω))) ≤ ∑ i, (H / universalH) * (score universalH L (m * q i) (W i ω) / (m : ℝ)) := by apply Finset.sum_le_sum intro i hi exact empiricalRadius_score_le_raw (q i) m hm H L hH hL (W i ω) _ = (H / universalH) * ((∑ i, score universalH L (m * q i) (W i ω)) / (m : ℝ)) := by rw [← Finset.mul_sum, Finset.sum_div] -
empiricalRadius_totalLocalScale_divtheorem — For finite intensities, positive exposure, and a level of at least one, the total raw local scale divided by exposure equals the normalized scale of the total intensity.hypothesesconclusionlocalScale (∑ i, m * q i) L / (m : ℝ)= sqrt ((∑ i, (q i : ℝ)) * L / (m : ℝ)) + L / (m : ℝ)Proof (Lean source)
-- Convert the NNReal sum of m*q_i to m times the NNReal sum q_i, apply -- empiricalRadius_localScale_div, and rewrite the cast of the sum. theorem empiricalRadius_totalLocalScale_div {ι : Type*} [Fintype ι] (q : ι → ℝ≥0) (m : ℝ≥0) (hm : 0 < m) (L : ℝ) (hL : 1 ≤ L) : localScale (∑ i, m * q i) L / (m : ℝ) = sqrt ((∑ i, (q i : ℝ)) * L / (m : ℝ)) + L / (m : ℝ) := by have hsum : (∑ i, m * q i) = m * (∑ i, q i) := by rw [Finset.mul_sum] rw [hsum, empiricalRadius_localScale_div (∑ i, q i) m hm L hL, NNReal.coe_sum]