OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedTreeMaximal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transverse maximal energy needs separation only on packets whose coefficients are nonzero. Restriction retains the original partial sums.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.partial_as_index_sum line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrict_nonzero_partial line 32

    Source documentation

    Removing zero coefficients leaves every actual partial sum unchanged.

    theorem restrict_nonzero_partial
    (Q : Finset P.PacketIndex) (t : ℝ)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (hc : ∀ q : P.PacketIndex, q∉Q → c q.1 q.2.1 q.2.2=0)
    (n : ℕ) (z : ℝ×ℝ) :
    (P.restrictPackets Q).physicalTreePartial t (fun j l v => c j l v.val) n z=
      P.physicalTreePartial t c n z := by
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreePartial

  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_supported_transverse_tree_maximal line 51