OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedTopPhysical.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The common-type assigned top families have exactly the original physical bands, including original selector coefficients and top masks.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopAlternate line 20
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopAlternate_bound line 26
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_assignedTopPackets_filter line 33
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_physicalMaskedValue line 42
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_physicalMaskedBand line 54
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_single_mask line 106

    Source documentation

    The mask on an assigned family is its single assigned top mask.

    theorem assignedTopFamily_single_mask (top : τ) (T : τ → SlopeBox) :
    (fun j (l : (P.assignedTopFamily packets assigned top).labels j)
      (u : P.AssignedTopItem packets assigned j l) =>
        T (assigned ⟨j,⟨l.val.2,u.val⟩⟩)) = fun _ _ _ => T top := by
…

    Mentions: OAI.LipschitzHilbert.SlopeBox

  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_topMaskBand line 114