SplitSupportedTarget.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Split an actual smooth compactly supported target using the finite smooth phase partition. Every piece is a supported smooth field on a compact subset of its phase domain, and the sum of the pieces is the original target.

def OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.pieceSupport line 31
Source documentation
Each target piece is supported both where the target was supported and where its partition coefficient is supported.
```
def pieceSupport (P : CompactPhasePartition ι (K : Set Base) U) (i : ι) :
    Compacts Base :=
…
```
Mentions: OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.coe_pieceSupport line 36
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.pieceSupport_subset_original line 39
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.pieceSupport_subset_domain line 42
def OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.splitSupported line 46
Source documentation
The piece is constructed by ordinary scalar multiplication of the target.
```
def splitSupported (P : CompactPhasePartition ι (K : Set Base) U)
    (A : SupportedField (F := F) K) (i : ι) : SupportedField (F := F) (P.pieceSupport i) :=
…
```
Mentions: OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.splitSupported_apply line 53
def OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.splitSupportedLM line 58
Source documentation
With the partition fixed, splitting is linear in the target.
```
def splitSupportedLM (P : CompactPhasePartition ι (K : Set Base) U) (i : ι) :
    SupportedField (F := F) K →ₗ[ℝ] SupportedField (F := F) (P.pieceSupport i) where
…
```
Mentions: OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.splitSupported_tsupport_subset line 72
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.sum_splitSupported_apply line 79
Source documentation
The finite pieces sum to the original target at every point, including outside the compact set on which the coefficients sum to one.
```
theorem sum_splitSupported_apply (P : CompactPhasePartition ι (K : Set Base) U)
    (A : SupportedField (F := F) K) (x : Base) :
…
```
Mentions: OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition
theorem OAI.ClosedSurfaceR4.PhasePartitions.CompactPhasePartition.sum_splitSupported line 88

theorem OAI.ClosedSurfaceR4.PhasePartitions.exists_split_supported_complex_target line 98

Source documentation

Split the actual complex tensor target into one smooth supported target for each supplied phase domain, without changing their total.

theorem exists_split_supported_complex_target {ι : Type*} [Fintype ι]
    (K : Compacts Base) (U : ι → Set Base) (hU : ∀ i, IsOpen (U i))
    (hcover : (K : Set Base) ⊆ ⋃ i, U i)
    (A : SupportedField (F := ComplexTensor) K) :
…