OAI/Probability/Subsphere/Regression/Gram.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereRegression.gram_linear_combination line 17
2. def OAI.SubsphereRegression.gsUpper line 31
3. lemma OAI.SubsphereRegression.gsUpper_expansion line 35
4. lemma OAI.SubsphereRegression.gsUpper_det line 46
5. lemma OAI.SubsphereRegression.gram_gramSchmidt_diagonal line 54
6. theorem OAI.SubsphereRegression.det_gram_eq_prod_gramSchmidt line 65

   Source documentation

   The Gram determinant is the product of the squared Gram--Schmidt lengths, including tuples containing dependent vectors.

   theorem det_gram_eq_prod_gramSchmidt (v : Fin n → E) :
       (Matrix.gram ℝ v).det = ∏ i, ‖gramSchmidt ℝ v i‖ ^ 2 := by
   …

7. lemma OAI.SubsphereRegression.sub_gramSchmidt_mem_span line 79
8. lemma OAI.SubsphereRegression.gramSchmidt_mem_span_orthogonal line 88
9. lemma OAI.SubsphereRegression.gramSchmidt_eq_sub_starProjection line 100
10. lemma OAI.SubsphereRegression.norm_gramSchmidt_eq_infDist line 108
11. lemma OAI.SubsphereRegression.infDist_affine_mk' line 115
12. lemma OAI.SubsphereRegression.norm_gramSchmidt_sub_eq_affine_infDist line 129
13. lemma OAI.SubsphereRegression.image_Iio_castSucc line 136
14. lemma OAI.SubsphereRegression.image_Iio_last line 147
15. lemma OAI.SubsphereRegression.gramSchmidt_castSucc line 156
16. lemma OAI.SubsphereRegression.measurable_gramSchmidt line 162
17. lemma OAI.SubsphereRegression.lintegral_pi_snoc line 184
18. def OAI.SubsphereRegression.replicaWeight line 204
19. lemma OAI.SubsphereRegression.measurable_replicaWeight line 207
20. lemma OAI.SubsphereRegression.replicaWeight_snoc line 214
21. def OAI.SubsphereRegression.replicaConstant line 224
22. lemma OAI.SubsphereRegression.affine_inverse_moment_le_replicaConstant line 228
23. theorem OAI.SubsphereRegression.replica_integral_bound line 242

    Source documentation

    Tonelli integration of the Gram--Schmidt inverse-distance product. The first replica p is fixed; n further replicas are integrated.

    theorem replica_integral_bound {ν : Measure E} [IsFiniteMeasure ν]
        {a : ℝ} (hν : HasLocalMassBound ν a)
        (hsupport : ν.support ⊆ Metric.closedBall 0 1) (m : ℕ) (p : E)
        (n : ℕ) (hmargin : (n : ℝ) + m ≤ a) :
        ∫⁻ v : Fin n → E, replicaWeight m p v ∂Measure.pi (fun _ => ν) ≤
          (replicaConstant ν a m) ^ n := by
    …

    Mentions: OAI.SubsphereRegression.HasLocalMassBound, OAI.SubsphereRegression.replicaWeight, OAI.SubsphereRegression.replicaConstant

24. lemma OAI.SubsphereRegression.ae_pi_snoc line 279
25. lemma OAI.SubsphereRegression.measurableSet_gramSchmidt_ne_zero line 304
26. theorem OAI.SubsphereRegression.ae_gramSchmidt_ne_zero line 314

    Source documentation

    Successive affine degeneracies have product measure zero.

    theorem ae_gramSchmidt_ne_zero {ν : Measure E} [IsFiniteMeasure ν]
        {a : ℝ} (hν : HasLocalMassBound ν a)
        (hsupport : ν.support ⊆ Metric.closedBall 0 1) (p : E)
        (n : ℕ) (hmargin : (n : ℝ) ≤ a) :
        ∀ᵐ v : Fin n → E ∂Measure.pi (fun _ => ν),
          ∀ i, gramSchmidt ℝ (fun j => v j - p) i ≠ 0 := by
    …

    Mentions: OAI.SubsphereRegression.HasLocalMassBound

27. theorem OAI.SubsphereRegression.ae_replica_linearIndependent line 351

    Source documentation

    The replica difference matrix has full column rank almost everywhere.

    theorem ae_replica_linearIndependent {ν : Measure E} [IsFiniteMeasure ν]
        {a : ℝ} (hν : HasLocalMassBound ν a)
        (hsupport : ν.support ⊆ Metric.closedBall 0 1) (p : E)
        (n : ℕ) (hmargin : (n : ℝ) ≤ a) :
        ∀ᵐ v : Fin n → E ∂Measure.pi (fun _ => ν),
          LinearIndependent ℝ (fun j => v j - p) := by
    …

    Mentions: OAI.SubsphereRegression.HasLocalMassBound

28. lemma OAI.SubsphereRegression.sqrt_det_gram line 363
29. lemma OAI.SubsphereRegression.replicaWeight_eq_det line 369
30. theorem OAI.SubsphereRegression.gram_integral_bound line 375