OAI/Analysis/LipschitzHilbert/Trees/SourceVectorEnvelope.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The reference-direction scalar envelope controls the actual componentwise packet synthesis without a frequency-dimension factor.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.packetVector line 16

    Source documentation

    A coefficient vector multiplying the original physical packet.

    def packetVector
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (q : P.PacketIndex) (z : ℝ×ℝ) : EuclideanSpace ℂ κ :=
…
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.packetVector_reference_envelope line 21
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.packet_sum_reference_envelope line 42