SourceAssignedStoppedBound.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The supported assigned-top estimates apply to the original individual physical packets. These identities retain their analyzing coefficients, alternate profiles, stopping levels, masks and source transitions.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedBand_const_eq_rawBand line 19

Source documentation

A constant top mask can be placed in the raw coefficients exactly.

theorem physicalMaskedBand_const_eq_rawBand (P : SourceLabeledLattice N κ Label Item)
    (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
    (t : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ) (v : ℝ×ℝ → ℝ)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (T : SlopeBox) (L A : ℝ)
    (z : ℝ×ℝ) (j : Fin N) :
    P.physicalMaskedBand alt hAlt t b v f (fun _ _ _ => T) L A (z.2-t*z.1) j z.1 =
      (P.withProfile alt hAlt).rawBand
        (fun j l u => T.mask L A z • P.physicalMultiplierCoefficient t b v f j l u)
        0 j z.1 (z.2-t*z.1) := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledLattice.rawBand

def OAI.LipschitzHilbert.SourceLabeledLattice.assignedReferenceFamily line 56
Source documentation
The common-type recentered family used in the actual top envelopes.
```
def assignedReferenceFamily (top : τ) :
    SourceLabeledLattice N κ (fun j => τ×P.labels j) (P.AssignedTopItem packets assigned) :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice
def OAI.LipschitzHilbert.SourceLabeledLattice.assignedReferenceOriginalLabel line 64
def OAI.LipschitzHilbert.SourceLabeledLattice.assignedReferenceAlternate line 74
theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedReferenceAlternate_bound line 82
def OAI.LipschitzHilbert.SourceLabeledLattice.assignedReferenceSelector line 93
theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedReference_rawBand_original line 99

theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedReference_packetAmplitude_original line 115

Source documentation

Original packets, their literal top/length fibers and the recentered raw bands have exactly the same source amplitude.

theorem assignedReference_packetAmplitude_original
    (grid : AngularGrid) (tops : Finset τ) (precision : τ → ℝ) (cut : ℝ)
    (weight : τ → (ℝ×ℝ) → ℝ) (K : ℕ) (gap : ℕ → ℝ)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (hcondition : ∀ q ∈ packets,
      P.referenceCondition oldSlope (T (assigned q)).slope (R (assigned q)) cone w q.1 q.2.1)
    (stop : τ → Fin N → ℕ) (phase : ℕ → ℂ) (a L A : ℝ)
    (z : ℝ×ℝ) (level : ℕ) (cell : ℤ) :
    grid.sourcePacketAmplitude tops (fun t => (T t).slope) precision cut weight K gap
      packets assigned (fun q => stop (assigned q) q.1)
      (P.physicalMaskedValue alt hAlt oldSlope b v f
        (fun j l u => T (assigned ⟨j,⟨l,u⟩⟩)) L A z) phase a z level cell =
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedReference_offchildAmplitude_original line 151

Source documentation

The exact off-child regrouping also retains original packet masks and coefficients; only the assignment fiber is summed.

theorem assignedReference_offchildAmplitude_original
    (grid : AngularGrid) (tops : Finset τ) (precision : τ → ℝ) (cut : ℝ)
    (weight : τ → (ℝ×ℝ) → ℝ) (K : ℕ) (gap : ℕ → ℝ)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (hcondition : ∀ q ∈ packets,
      P.referenceCondition oldSlope (T (assigned q)).slope (R (assigned q)) cone w q.1 q.2.1)
    (stop : τ → Fin N → ℕ) (phase : ℕ → ℂ) (a L A : ℝ)
    (z : ℝ×ℝ) (level : ℕ) (cell : ℤ) (child : Finset τ) :
    grid.sourcePacketAmplitude tops (fun t => (T t).slope) precision cut weight K gap
      (packets.filter (fun u => assigned u ∉ child)) assigned (fun q => stop (assigned q) q.1)
      (P.physicalMaskedValue alt hAlt oldSlope b v f
        (fun j l u => T (assigned ⟨j,⟨l,u⟩⟩)) L A z) phase a z level cell =
…

Mentions: OAI.LipschitzHilbert.AngularGrid