OAI/Probability/Subsphere/Mixture/Domination.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereCurrent.Mixture.block_classification line 14
2. lemma OAI.SubsphereCurrent.Mixture.mixtureLaw_mono line 47
3. lemma OAI.SubsphereCurrent.Mixture.mixtureLaw_add line 51
4. lemma OAI.SubsphereCurrent.Mixture.mixtureLaw_smul line 55
5. lemma OAI.SubsphereCurrent.Mixture.mixtureLaw_domination line 60
6. def OAI.SubsphereCurrent.betaRaw line 74
7. lemma OAI.SubsphereCurrent.betaRaw_eq line 77
8. lemma OAI.SubsphereCurrent.lintegral_betaRaw line 86
9. lemma OAI.SubsphereCurrent.beta_antitone_left line 93
10. lemma OAI.SubsphereCurrent.beta_antitone_right line 106
11. lemma OAI.SubsphereCurrent.rpow_decrease_shift line 112
12. lemma OAI.SubsphereCurrent.betaPDFReal_domination_right_half line 133
13. lemma OAI.SubsphereCurrent.betaPDFReal_domination_left_half line 154
14. theorem OAI.SubsphereCurrent.betaMeasure_two_component line 173
15. theorem OAI.SubsphereCurrent.Mixture.directionLaw_domination line 208

    Source documentation

    The full geometric two-component domination, not just a scalar-density bound.

    theorem directionLaw_domination (V N : Submodule ℝ E) (hVN : V ≤ N)
        (hj : 1 ≤ Module.finrank ℝ V) (hjn : Module.finrank ℝ V < Module.finrank ℝ N)
        (hnD : Module.finrank ℝ N < Module.finrank ℝ E) (e : Metric.sphere (0 : V) 1) :
        directionLaw V N ≤ (2 : ℝ≥0∞)^Module.finrank ℝ E •
          (SubsphereRegression.ambientSphereLaw + latitudeLaw V e
            (((Module.finrank ℝ N : ℝ)-(Module.finrank ℝ V : ℝ))/2)
            (((Module.finrank ℝ E : ℝ)-(Module.finrank ℝ N : ℝ))/2)) := by
    …

    Mentions: OAI.SubsphereCurrent.Mixture.directionLaw, OAI.SubsphereRegression.ambientSphereLaw, OAI.SubsphereCurrent.Mixture.latitudeLaw

16. lemma OAI.SubsphereCurrent.Mixture.ambientSphereLaw_transport line 296
17. lemma OAI.SubsphereCurrent.Mixture.block_bottom_haar line 317
18. lemma OAI.SubsphereCurrent.Mixture.directionLaw_bottom line 330
19. lemma OAI.SubsphereCurrent.Mixture.measurable_directionJointSampler line 346
20. lemma OAI.SubsphereCurrent.Mixture.directionJointLaw_top line 354
21. theorem OAI.SubsphereCurrent.Mixture.mixture_estimate line 384