OAI/Probability/Subsphere/Regression/Projection.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubsphereRegression.matrixLabelReference line 18
2. def OAI.SubsphereRegression.projectionLaw line 21
3. def OAI.SubsphereRegression.gaussianCoupling line 25
4. def OAI.SubsphereRegression.noisyObservation line 30
5. lemma OAI.SubsphereRegression.measurable_noisyObservation line 34
6. lemma OAI.SubsphereRegression.gaussianCoupling_map_noisyObservation_zero line 39
7. lemma OAI.SubsphereRegression.gaussianCoupling_map_noisyObservation line 54

   Source documentation

   The smoothed projection really is the density of the coupled noisy law.

   lemma gaussianCoupling_map_noisyObservation (ν : Measure E) [SigmaFinite ν]
       (m : ℕ) (δ : ℝ) (hδ : δ ≠ 0) :
       (gaussianCoupling ν m).map (noisyObservation m δ) =
         (matrixLabelReference (E := E) m).withDensity
   …

   Mentions: OAI.SubsphereRegression.gaussianCoupling, OAI.SubsphereRegression.noisyObservation, OAI.SubsphereRegression.matrixLabelReference

8. lemma OAI.SubsphereRegression.matrixLabelReference_outerRegular line 78
9. lemma OAI.SubsphereRegression.tendsto_noisyObservation line 85
10. theorem OAI.SubsphereRegression.projectionLaw_set_bound line 95
11. def OAI.SubsphereRegression.coordinateNorm line 138

    Source documentation

    The Euclidean norm of an ordinary finite coordinate tuple.

    def coordinateNorm {m : ℕ} (y : Fin m → ℝ) : ℝ := ‖WithLp.toLp 2 y‖

12. lemma OAI.SubsphereRegression.continuous_coordinateNorm line 140
13. lemma OAI.SubsphereRegression.coordinateNorm_sq line 145
14. lemma OAI.SubsphereRegression.coordinateNorm_smul line 149
15. def OAI.SubsphereRegression.coordinateBall line 153
16. lemma OAI.SubsphereRegression.measurableSet_coordinateBall line 156
17. lemma OAI.SubsphereRegression.coordinateBall_smul line 160
18. lemma OAI.SubsphereRegression.volume_coordinateBall_smul line 174
19. lemma OAI.SubsphereRegression.gaussianPDF_le_exp line 180
20. lemma OAI.SubsphereRegression.lintegral_quarterGaussian_le line 190
21. lemma OAI.SubsphereRegression.gaussian_density_pair_bound line 208
22. lemma OAI.SubsphereRegression.measurable_coordinateVolume line 236
23. lemma OAI.SubsphereRegression.gaussian_expected_coordinate_volume line 248
24. lemma OAI.SubsphereRegression.stdGaussian_inner_map line 295
25. lemma OAI.SubsphereRegression.rows_inner_map line 310
26. lemma OAI.SubsphereRegression.rows_expected_coordinate_volume line 320
27. def OAI.SubsphereRegression.rowOperator line 339

    Source documentation

    Linear noiseless observation operator, with the Euclidean output norm.

    def rowOperator {m : ℕ} (A : Fin m → E) : E →L[ℝ] EuclideanSpace ℝ (Fin m) :=
    …

28. lemma OAI.SubsphereRegression.rowOperator_apply line 344
29. def OAI.SubsphereRegression.netProjectionSupport line 350

    Source documentation

    A measurable common support enclosure indexed by a finite input net.

    def netProjectionSupport (s : Finset E) (m : ℕ) :
        Set ((Fin m → E) × (Fin m → ℝ)) :=
    …

30. lemma OAI.SubsphereRegression.measurableSet_netProjectionSupport line 354
31. lemma OAI.SubsphereRegression.netProjectionSupport_volume line 360
32. lemma OAI.SubsphereRegression.opNorm_le_twice_net line 388
33. theorem OAI.SubsphereRegression.exists_projection_support line 416

    Source documentation

    Common finite-volume enclosure of every noiseless observation from the unit ball. The constant is exponential in input dimension, uniformly over m ≤ d.

    theorem exists_projection_support (m : ℕ) (hm : m ≤ Module.finrank ℝ E) :
        ∃ D : Set ((Fin m → E) × (Fin m → ℝ)), MeasurableSet D ∧
          (∀ A t, ‖t‖ ≤ 1 → (A, fun j => ⟪t, A j⟫) ∈ D) ∧
          matrixLabelReference (E := E) m D ≤ (192 : ℝ≥0∞)^(Module.finrank ℝ E) := by
    …

    Mentions: OAI.SubsphereRegression.matrixLabelReference