DenseDifferences.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Dense pairwise differences in the norm-closed difference span

All closures use the given norm topology. Density in the norm subtype of K is transported through the continuous subtraction map on K × K. No completeness, convexity, closedness or compactness assumption is needed.

theorem OAI.ReflexiveFixedPoints.pairwiseDifferences_subset_sub line 21

theorem OAI.ReflexiveFixedPoints.pairwiseDifferences_subset_closure line 28

Source documentation

Every actual difference is approximated by differences of the dense sequence.

theorem pairwiseDifferences_subset_closure {X : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] {K : Set X} (z : ℕ → K) (hz : DenseRange z) :
    K - K ⊆ closure (Set.range (fun ij : ℕ × ℕ => (z ij.1 : X) - (z ij.2 : X))) := by
…

theorem OAI.ReflexiveFixedPoints.closure_span_pairwiseDifferences line 44

Source documentation

The sampled pairwise differences generate the entire norm-closed difference span.

theorem closure_span_pairwiseDifferences (z : ℕ → K) (hz : DenseRange z) :
    (Submodule.span ℝ
      (Set.range (fun ij : ℕ × ℕ => (z ij.1 : X) - (z ij.2 : X)))).topologicalClosure =
      (Submodule.span ℝ (K - K)).topologicalClosure := by
…

theorem OAI.ReflexiveFixedPoints.closure_span_pairwiseDifferences_eq_differenceSpan line 58

Source documentation

The same equality with the shared reduction carrier.

theorem closure_span_pairwiseDifferences_eq_differenceSpan
    (z : ℕ → K) (hz : DenseRange z) :
    (Submodule.span ℝ
      (Set.range (fun ij : ℕ × ℕ => (z ij.1 : X) - (z ij.2 : X)))).topologicalClosure =
      differenceSpan K :=
…

Mentions: OAI.ReflexiveFixedPoints.differenceSpan