ProductFactorDiameter.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The residual factor of a full-dimensional product approximation is small

An orthogonal simplex in the Euclidean factor together with one point in the other factor gives an explicit dimension obstruction. This is the geometric bridge needed after the product conclusion of Huang--Huang Theorem 2.9(2).

theorem OAI.RegularPointCoordinates.metric_prod_dist_L2 line 20
theorem OAI.RegularPointCoordinates.scaled_unit_dist_zero line 26
theorem OAI.RegularPointCoordinates.scaled_units_dist line 31

theorem OAI.RegularPointCoordinates.product_factor_distance_le line 49

Source documentation

Points of the residual factor inside the unit ball must be close to its base point when the same ball also approximates R^n.

theorem product_factor_distance_le {X Z : Type*} [MetricSpace X] [MetricSpace Z]
    (n : ℕ) {p : X} {z₀ z : Z} {r δ η : ℝ} (hr : 0 < r) (hδ : 0 ≤ δ)
    (hη : 0 ≤ η) (hη1 : η ≤ 1) (hz : dist z z₀ ≤ 1)
    (f : X → Euclidean n) (g : X → WithLp 2 (Euclidean n × Z))
    (hf : IsPointedApproximation p 0 r 2 δ f)
    (hg : IsPointedApproximation p (WithLp.toLp 2 (0, z₀)) r 2 η g) :
    dist z z₀ ≤ 10 * ((n + 1 : ℕ) : ℝ) ^ 2 * (δ + 3 * η) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation

theorem OAI.RegularPointCoordinates.metric_prod_dist_error line 117
theorem OAI.RegularPointCoordinates.metric_prod_same_second line 130

theorem OAI.RegularPointCoordinates.product_projection_approximation line 139

Source documentation

Projection of a full-dimensional product approximation is itself a pointed Euclidean approximation on the inner half-ball.

theorem product_projection_approximation {X Z : Type*} [MetricSpace X] [MetricSpace Z]
    (n : ℕ) {p : X} {z₀ : Z} {r δ η : ℝ} (hr : 0 < r) (hδ : 0 ≤ δ)
    (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 4)
    (f : X → Euclidean n) (g : X → WithLp 2 (Euclidean n × Z))
    (hf : IsPointedApproximation p 0 r 2 δ f)
    (hg : IsPointedApproximation p (WithLp.toLp 2 (0, z₀)) r 2 η g) :
    IsPointedApproximation p 0 r (1 / 2)
      (η + 20 * ((n + 1 : ℕ) : ℝ) ^ 2 * (δ + 3 * η)) (fun x => (g x).fst) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation