ProductProjectionSmallFactor.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Projecting a product approximation with a small residual fiber

theorem OAI.RegularPointCoordinates.product_dist_le_sum line 11

theorem OAI.RegularPointCoordinates.product_projection_small_factor line 23

Source documentation

A small residual fiber suffices for a coordinate approximation on a fixed inner ball. The larger source ball is retained for target density.

theorem product_projection_small_factor {X Z : Type*} [MetricSpace X] [MetricSpace Z]
    {n : ℕ} {p : X} {z₀ : Z} {r ε a : ℝ} (hr : 0 < r) (he : 0 ≤ ε)
    (he16 : ε ≤ 1/16) (ha : 0 ≤ a)
    {f : X → WithLp 2 (Euclidean n × Z)}
    (hf : IsPointedApproximation p (WithLp.toLp 2 (0,z₀)) r 1 ε f)
    (hsmall : ∀ z : Z, dist z₀ z ≤ 1/4 → dist z₀ z ≤ a) :
    IsPointedApproximation p 0 r (1/16) (3*ε+2*a) (fun x => (f x).fst) := by
…

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