PacketDataAssignedTopEnvelope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Only nonempty assigned scales impose a reference length restriction.

theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_supported_length line 28
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.PacketLatticeData.length

theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_topMaskBand_all line 41

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.PacketLatticeData.physicalMaskedBand

theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopReference_interval_norm_of_joint line 68

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.PacketLatticeData.withProfile