SourceCarrierFreeEnvelope.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The positive error envelope must not inherit the large carrier bound of the wide reference cone. The exact raw norm is independent of it.

theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_joint_measurable line 14
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_swapped_joint_measurable line 21
def OAI.LipschitzHilbert.SourceLatticePacket.absoluteConstant line 31
Source documentation
The absolute raw-envelope constant contains no frequency or carrier.
```
def absoluteConstant (P : SourceLatticePacket N κ ι) : ℝ :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLatticePacket
theorem OAI.LipschitzHilbert.SourceLatticePacket.absoluteConstant_pos line 34
theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_absolute_lattice_envelope line 40

theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_absolute_tileEnvelope line 53

Source documentation

This is the envelope used by the original positive angular-error convolution estimate, on the original snapped lattice.

theorem raw_absolute_tileEnvelope (P : SourceLatticePacket N κ ι) (horder : 6 ≤ P.order)
    (i : Fin 3) (j : Fin N) (u : ι j) (k : κ) (z : ℝ×ℝ) :
    ‖P.raw i j u k z.2 z.1‖ ≤ P.absoluteConstant*
      tileEnvelope (P.length j*(P.snappedSite j u).1)
        (P.width*(P.snappedSite j u).2) (P.length j) P.width 6 z := by
…

Mentions: OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.tileEnvelope