OAI/Analysis/LipschitzHilbert/Trees/SourceSelectedFamily.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A selected packet set as its exact finite lattice family. Empty labels are removed, so row bounds follow from actual selected packets.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.selectedLabels line 17
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.selectedOriginalLabel line 21
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily line 25
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.selectedPacketEquiv line 54
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_mem line 65
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedLabel_has_packet line 71
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_length line 77
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_physicalPacket line 80
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_absoluteConstant line 86
  10. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_selectedFamily line 89
  11. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_energy line 96
  12. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_actualX line 107
  13. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_actualZ line 111
  14. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_selector_value line 115
  15. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_separated_energy line 129
  16. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_ordinaryDensity line 142
  17. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedFamily_card_le_local line 151

    Source documentation

    Local angular multiplicity bounds the number of occupied rows in a selected tree, independent of its original ambient labels.

    theorem selectedFamily_card_le_local (Q : Finset P.PacketIndex) (w t cone : ℝ)
    (hw : 0<w) (M K : ℕ) (hK : cone≤K)
    (hcone : ∀ q∈Q, |P.rowSlope q.1 q.2.1-t|≤cone*(w/P.length q.1))
    (j : Fin N)
    (hlocal : SourceSlopeLabels.LocalMultiplicity Finset.univ
      (fun l : P.labels j => P.rowSlope j l) (w/P.length j) M) :
    ((P.selectedFamily Q).labels j).card≤(2*K+1)*M := by
…

    Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity