OAI/NumberTheory/DukePrimeDegree/Geometry/ProjectionFromDistances.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recovering measurable orthogonal projections from distances

Polarization expresses every scalar coordinate of an orthogonal projection using four distances to the subspace. This avoids an assumed measurable choice of bases. It will be applied to the actual component velocity spaces after their distance functions have been constructed.

  1. lemma OAI.DukePrimeDegree.infDist_eq_norm_sub_starProjection line 24
  2. lemma OAI.DukePrimeDegree.norm_starProjection_sq_eq line 32
  3. theorem OAI.DukePrimeDegree.inner_starProjection_from_distances line 43

    Source documentation

    A coordinate of the projection is determined by the squared projection norms at the sum and difference of two fixed vectors.

    theorem inner_starProjection_from_distances (W : Submodule ℝ E)
    [W.HasOrthogonalProjection] (v w : E) :
    ⟪W.starProjection v, w⟫_ℝ =
      ((‖v + w‖ ^ 2 - Metric.infDist (v + w) (W : Set E) ^ 2) -
        (‖v - w‖ ^ 2 - Metric.infDist (v - w) (W : Set E) ^ 2)) / 4 := by
…
  4. theorem OAI.DukePrimeDegree.measurable_inner_starProjection_of_distances line 61