OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledSynthesisEnvelope.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pointwise norms of actual vector packets are controlled by the same positive main and error envelopes used in the reference tails.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.positiveEnvelope line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.positiveEnvelope_nonneg line 20
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.tileEnvelope_le_positive line 24
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.rawPacketValue line 32
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_packet_value_norm line 36
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_packet_value_split line 46
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_raw_packet_values_split line 67

    Source documentation

    Every path-dependent packet subset is bounded by the one fixed positive reference family.

    theorem sum_raw_packet_values_split (horder : 6 ≤ P.order) (i : Fin 3) (j : Fin N)
    (c main error : ∀ l : P.labels j, Item j l → EuclideanSpace ℂ κ)
    (hsplit : ∀ l u, c l u = main l u+error l u)
    (Q : Finset (Σ l : P.labels j, Item j l)) (y x : ℝ) :
    (∑ q ∈ Q, ‖P.rawPacketValue i j q.1 q.2 (c q.1 q.2) y x‖) ≤
      P.absoluteConstant*((∑ l : P.labels j, ∑ u : Item j l,
        ‖error l u‖*tileEnvelope (P.length j*(P.snappedSite j l u).1)
          (P.width*(P.snappedSite j l u).2) (P.length j) P.width 6 (x,y))+
        ∑ l : P.labels j, ∑ u : Item j l, ‖main l u‖*P.positiveEnvelope j l u y x) := by
…

    Mentions: OAI.LipschitzHilbert.tileEnvelope