Theorems · Definition · probability
ProbabilityTheory.Fernique.normThreshold
ℝ → ℕ → ℝ
A sequence of real thresholds that will be used to cut the space into annuli.
Chosen such that for a rotation invariant measure, an application of lemma
measure_le_mul_measure_gt_le_of_map_rotation_eq_self gives
μ {x | ‖x‖ ≤ a} * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by14
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Fernique.lintegral_closedBall_sdiff_exp_logRatio_mul_sq_lestatement and proof · cited by 2
- ProbabilityTheory.Fernique.lt_normThreshold_zerostatement · cited by 2
- ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mulproof · cited by 1
- ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_lestatement and proof · cited by 1
- ProbabilityTheory.Fernique.measure_gt_normThreshold_le_expstatement · cited by 1
- ProbabilityTheory.Fernique.measure_gt_normThreshold_le_rpowstatement and proof · cited by 1
- ProbabilityTheory.Fernique.measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_selfstatement and proof · cited by 1
- ProbabilityTheory.Fernique.normThreshold_eqstatement · cited by 1
- ProbabilityTheory.Fernique.normThreshold_strictMonostatement · cited by 1
- ProbabilityTheory.Fernique.sq_normThreshold_add_one_lestatement · cited by 1
- ProbabilityTheory.Fernique.tendsto_normThreshold_atTopstatement · cited by 1
- ProbabilityTheory.Fernique.lintegral_closedBall_diff_exp_logRatio_mul_sq_lestatement · cited by 0