HitNormTopology.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Real-valued hit norms, their dual finite tests, and uniform strict inequalities over compact configuration spaces. These are the topological estimates used in the finite split of path-law fusion.

theorem OAI.CircleDomainRigidity.pathHitReal_upperSemicontinuous line 22
theorem OAI.CircleDomainRigidity.hasHitNormBound_iff_sum_sq_le line 34
theorem OAI.CircleDomainRigidity.isOpen_forall_compact_upper_bound line 55
Source documentation
For compact configurations, a joint upper semicontinuous strict bound persists on an open set of centers. This is the neighborhood step of the finite split.
```
theorem isOpen_forall_compact_upper_bound {Z T : Type*}
    [TopologicalSpace Z] [TopologicalSpace T] [CompactSpace T]
    {f : Z × T → ℝ} (hf : UpperSemicontinuous f) (C : ℝ) :
    IsOpen {z | ∀ t, f (z, t) < C} := by
…
```
theorem OAI.CircleDomainRigidity.upperSemicontinuous_nonnegative_mul line 66