SourceAssignedTopEnvelope.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Assigned packets need length bounds only on their nonempty scales. Clipping empty-scale stopping levels preserves the exact source amplitude. The original-selector concentration then supplies the needed intervals.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawBand_eq_zero_of_no_item line 19

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_stop_congr_of_zero line 39

Source documentation

Stopping times may change freely for zero packets.

theorem sourcePacketAmplitude_stop_congr_of_zero
    (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
    (cut : ℝ) (weight : ι → X → ℝ) (K : ℕ) (gap : ℕ → ℝ)
    (packets : Finset σ) (assigned : σ → ι) (stop stop' : σ → ℕ) (value : σ → E)
    (phase : ℕ → ℂ) (a : ℝ) (z : X) (level : ℕ) (cell : ℤ)
    (h : ∀ p ∈ packets, stop p = stop' p ∨ value p = 0) :
    g.sourcePacketAmplitude tops slope precision cut weight K gap packets assigned stop
      value phase a z level cell =
    g.sourcePacketAmplitude tops slope precision cut weight K gap packets assigned stop'
      value phase a z level cell := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_supported_selector_node_envelope line 56
theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_supported_length line 210
Source documentation
Empty long scales impose no artificial restriction on the global longest-scale field. Every retained packet has the true assigned length.
```
theorem assignedTopReference_supported_length
    (hshort : ∀ q ∈ packets, P.length q.1 ≤ (T (assigned q)).length)
    (j : Fin N) (l : (Q).labels j) (u : P.AssignedTopItem packets assigned j l) :
    (Q).length j ≤ (T top).length := by
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.length

theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_topMaskBand_all line 223

Source documentation

The supported assigned/reference bands remain the original physical synthesis with its original top mask, including empty scales.

theorem assignedTopReference_topMaskBand_all
    (hcondition : ∀ q ∈ packets, assigned q = top →
      P.referenceCondition oldSlope (T top).slope R cone w q.1 q.2.1)
    (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)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (v : ℝ×ℝ → ℝ)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (L maskExponent : ℝ) (z : ℝ×ℝ) (j : Fin N) :
    (Q).physicalMaskedBand
      (fun j l u k => alt j (orig j l).val.2 u.val k)
      (fun j l u k => hAlt j (orig j l).val.2 u.val k)
      (T top).slope (fun j l => b j (orig j l).val.2) v f
      (fun _ _ _ => T top) L maskExponent (z.2-(T top).slope*z.1) j z.1 =
…

Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedBand

theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopReference_interval_norm_of_joint line 250

Source documentation

The joint estimate returned by assigned-top concentration supplies the interval premise of the supported envelope and off-child lemmas.

theorem assignedTopReference_interval_norm_of_joint
    (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)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (v : ℝ×ℝ → ℝ)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (A Kw D : ℝ) (z : ℝ×ℝ)
    (hjoint : ∀ lower upper, lower ≤ upper → upper ≤ N →
      let V := fun x y => ((Q).withProfile
…

Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SourceLabeledLattice.withProfile