OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledVariationSplit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The fixed masked variation uses the full original analyzing coefficients. Its centered main part has the narrow-slot variation bound; its angular error is bounded by the positive physical error sum, using the carrier-free synthesis envelope.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedBand line 24
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalErrorMaskedBand line 30
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedVariation line 36
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedBand_physical_continuous line 40
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedVariation_physical_continuous line 55
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedBand_split line 68
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.masked_packet_norm line 89
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalErrorMaskedBand_norm_le line 115
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedVariation_le_main_add_error line 146

    Source documentation

    The full original masked sequence has the narrow main variation plus the single carrier-free positive angular-error sum.

    theorem physicalMaskedVariation_le_main_add_error (horder : 6 ≤ P.order)
    (hb : ∀ j l k, Measurable (b j l k))
    (hb1 : ∀ j l k s, ‖b j l k s‖ ≤ 1)
    (hv : Measurable v) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1) (x : ℝ) :
    P.physicalMaskedVariation alt hAlt t b v g T L A y x ≤
      P.physicalCenteredMaskedVariation alt hAlt t a b v g T L A y x+
        P.absoluteConstant*P.physicalAngularError t a b v g (x,y+t*x) := by
…