CompactPhaseWeights.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive frequency weights giving good sums and differences on the actual compact pairwise phase supports.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.finite_set_compact_good_weights line 13

theorem OAI.ClosedSurfaceR4.PhaseGeometry.finite_compact_good_weights line 71

Source documentation

One fixed positive weight for each member of an arbitrary finite phase family makes all distinct pairwise sums and differences good on their prescribed symmetric compact supports.

theorem finite_compact_good_weights {ι X : Type*} [Finite ι] [TopologicalSpace X] {n : ℕ}
    (K : ι → ι → Set X) (hK : ∀ a b, IsCompact (K a b))
    (hKs : ∀ a b, K a b = K b a)
    (B : X → Fin 3 → RVec n) (ξ : ι → X → Base)
    (hB : Continuous B) (hξ : ∀ a, Continuous (ξ a))
    (hgood : ∀ a b, a ≠ b → ∀ x ∈ K a b, Good (B x) (ξ a x)) :
    ∃ w : ι → ℝ, (∀ a, 0 < w a) ∧
      ∀ a b, a ≠ b → ∀ x ∈ K a b,
        Good (B x) (w a • ξ a x + w b • ξ b x) ∧
        Good (B x) (w a • ξ a x - w b • ξ b x) := by
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.Good