CompactPhasePartition.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite smooth partitions on the compact set on which a phase correction is required. The coefficients have compact support inside the supplied open phase domains. These are ordinary partition coefficients, so splitting a tensor target does not require taking square roots.

structure OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition line 24
Source documentation
A finite smooth partition on a compact target set, with compact supports subordinate to the prescribed phase domains.
```
structure CompactPhasePartition (ι : Type*) [Fintype ι]
    (K : Set Base) (U : ι → Set Base) where
…
```
def OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.supportCompact line 39
Source documentation
The actual compact topological support of one partition coefficient.
```
def supportCompact (P : CompactPhasePartition ι K U) (i : ι) : Compacts Base :=
…
```
Mentions: OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.coe_supportCompact line 42
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.supportCompact_subset line 45
theorem OAI.ClosedSurfaceR4.PhasePartitions.exists_compact_phase_partition line 52
Source documentation
A finite open cover of a compact subset of the phase plane admits compactly supported smooth partition coefficients indexed by that same cover.
```
theorem exists_compact_phase_partition {ι : Type*} [Fintype ι]
    {K : Set Base} (hK : IsCompact K) (U : ι → Set Base)
    (hU : ∀ i, IsOpen (U i)) (hcover : K ⊆ ⋃ i, U i) :
    Nonempty (CompactPhasePartition ι K U) := by
…
```
Mentions: OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition
theorem OAI.ClosedSurfaceR4.PhasePartitions.exists_finite_compact_phase_partition line 83
Source documentation
For a family of local phase domains, compactness first selects finitely many domains and then constructs the supported partition on those domains.
```
theorem exists_finite_compact_phase_partition {ι : Type*}
    {K : Set Base} (hK : IsCompact K) (U : ι → Set Base)
    (hU : ∀ i, IsOpen (U i)) (hcover : K ⊆ ⋃ i, U i) :
    ∃ s : Finset ι, Nonempty (CompactPhasePartition s K (fun i => U i)) := by
…
```
Mentions: OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition