OAI/Probability/Subsphere/Regression/Geometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereRegression.inverse_pow_dyadic_majorant line 17
2. lemma OAI.SubsphereRegression.dyadic_power_cancel line 52
3. theorem OAI.SubsphereRegression.inverse_moment_of_tube_bound line 64
4. def OAI.SubsphereRegression.HasLocalMassBound line 111
5. theorem OAI.SubsphereRegression.HasLocalMassBound.any_center line 117

   Source documentation

   Moving the center off the support costs a factor two in the radius.

   theorem HasLocalMassBound.any_center {ν : Measure E} {a : ℝ}
       (hν : HasLocalMassBound ν a) (z : E) {r : ℝ} (hr : 0 < r) :
       ν (Metric.closedBall z r) ≤ ENNReal.ofReal ((2 * r) ^ a) := by
   …

   Mentions: OAI.SubsphereRegression.HasLocalMassBound

6. theorem OAI.SubsphereRegression.card_le_volume_ratio line 133

   Source documentation

   The elementary disjoint-ball packing bound, with its dimension dependence.

   theorem card_le_volume_ratio (s : Finset E) {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
       (hs : ∀ x ∈ s, ‖x‖ ≤ R)
       (hsep : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → r ≤ dist x y) :
       (s.card : ℝ) ≤ ((R + r / 2) / (r / 2)) ^ Module.finrank ℝ E := by
   …

7. theorem OAI.SubsphereRegression.exists_net_of_finite_packing_bound line 183

   Source documentation

   A bounded finite-packing cardinality gives a finite net, by adding a point if a cardinality-maximizing separated set does not yet cover.

   theorem exists_net_of_finite_packing_bound (A : Set E) {r : ℝ} (hr : 0 ≤ r) (N : ℕ)
       (hcard : ∀ s : Finset E, (∀ x ∈ s, x ∈ A) →
         (∀ x ∈ s, ∀ y ∈ s, x ≠ y → r < dist x y) → s.card ≤ N) :
       ∃ s : Finset E, (∀ x ∈ s, x ∈ A) ∧
         (∀ x ∈ s, ∀ y ∈ s, x ≠ y → r < dist x y) ∧
         ∀ x ∈ A, ∃ y ∈ s, dist x y ≤ r := by
   …

8. theorem OAI.SubsphereRegression.exists_unit_ball_net line 235

   Source documentation

   A quantitative net of the unit ball. This is the packing estimate used in the affine-tube and projected-support estimates, with no asymptotic notation.

   theorem exists_unit_ball_net {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) :
       ∃ s : Finset E, (∀ x ∈ s, ‖x‖ ≤ 1) ∧
         (s.card : ℝ) ≤ (3 / r) ^ Module.finrank ℝ E ∧
         ∀ x : E, ‖x‖ ≤ 1 → ∃ y ∈ s, dist x y ≤ r := by
   …

9. theorem OAI.SubsphereRegression.exists_affine_tube_cover line 267

   Source documentation

   Cover the tube inside the unit ball by a dimension-controlled finite family of ambient balls. The centers need not lie in the support of the measure.

   theorem exists_affine_tube_cover (L : AffineSubspace ℝ E) [Nonempty L]
       {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) :
       ∃ s : Finset L.direction,
         (s.card : ℝ) ≤ (3 / r) ^ Module.finrank ℝ L.direction ∧
         ∀ t : E, ‖t‖ ≤ 1 → Metric.infDist t L ≤ r →
           ∃ y ∈ s, dist t ((y : E) + (orthogonalProjection L 0 : E)) ≤ 2 * r := by
   …

10. theorem OAI.SubsphereRegression.HasLocalMassBound.affine_tube line 300

    Source documentation

    The precise affine-tube estimate, before combining its radius powers.

    theorem HasLocalMassBound.affine_tube {ν : Measure E} {a : ℝ}
        (hν : HasLocalMassBound ν a) (hsupport : ν.support ⊆ Metric.closedBall 0 1)
        (L : AffineSubspace ℝ E) [Nonempty L] {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) :
        ν {t | Metric.infDist t L ≤ r} ≤
          ENNReal.ofReal ((3 / r) ^ Module.finrank ℝ L.direction * (4 * r) ^ a) := by
    …

    Mentions: OAI.SubsphereRegression.HasLocalMassBound

11. lemma OAI.SubsphereRegression.tube_radius_factors line 331

    Source documentation

    Collecting the radius factors in the packing estimate.

    lemma tube_radius_factors (ℓ : ℕ) (a : ℝ) {r : ℝ} (hr : 0 < r) :
        (3 / r) ^ ℓ * (4 * r) ^ a =
          (3 : ℝ) ^ ℓ * (4 : ℝ) ^ a * r ^ (a - ℓ) := by
    …

12. theorem OAI.SubsphereRegression.HasLocalMassBound.affine_tube_pow line 339

    Source documentation

    An explicit positive margin reduces the tube estimate to an integer power.

    theorem HasLocalMassBound.affine_tube_pow {ν : Measure E} {a : ℝ}
        (hν : HasLocalMassBound ν a) (hsupport : ν.support ⊆ Metric.closedBall 0 1)
        (L : AffineSubspace ℝ E) [Nonempty L] (k : ℕ)
        (hmargin : (Module.finrank ℝ L.direction : ℝ) + k ≤ a)
        {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) :
        ν {t | Metric.infDist t L ≤ r} ≤
          ENNReal.ofReal ((3 : ℝ) ^ Module.finrank ℝ L.direction * (4 : ℝ) ^ a) *
            ENNReal.ofReal (r ^ k) := by
    …

    Mentions: OAI.SubsphereRegression.HasLocalMassBound

13. theorem OAI.SubsphereRegression.HasLocalMassBound.affine_inverse_moment line 354
14. theorem OAI.SubsphereRegression.HasLocalMassBound.affine_null line 368

    Source documentation

    Positive tube margin forces the affine plane itself to be null.

    theorem HasLocalMassBound.affine_null {ν : Measure E} {a : ℝ}
        (hν : HasLocalMassBound ν a) (hsupport : ν.support ⊆ Metric.closedBall 0 1)
        (L : AffineSubspace ℝ E) [Nonempty L]
        (hmargin : (Module.finrank ℝ L.direction : ℝ) + 1 ≤ a) : ν L = 0 := by
    …

    Mentions: OAI.SubsphereRegression.HasLocalMassBound