SourceMaskedVariationTail.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The masked reference variation tail in original physical variables. The interval may have any origin and any positive length containing the retained packet lengths. Neither its scale nor its origin enters the relative exceptional-measure constant.

def OAI.LipschitzHilbert.SourceLatticePacket.physicalMaskedBand line 24
def OAI.LipschitzHilbert.SourceLatticePacket.physicalMaskedVariation line 30
theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalMaskedBand_eq_reference line 35
theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalMaskedVariation_normalization line 42
theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalMaskedVariation_continuous line 63

theorem OAI.LipschitzHilbert.SourceLatticePacket.physical_masked_variation_tail line 86

Source documentation

The actual physical masked variation has an arbitrary exponential tail at a fixed polynomial threshold, uniformly over packet and interval scales. The exceptional event is measurable by the exact normalization.

theorem physical_masked_variation_tail (hVariation : LepingleInput)
    {lo hi : ℝ} (hlo : 0 < lo) (hhi : 0 ≤ hi)
    (q J A cone : ℝ) (hq : 0 ≤ q) (hJ : 0 ≤ J) (hA : 1 < A) (hcone : 0 ≤ cone) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι),
      P.constant ≤ L^q →
    ∀ (c : ∀ j, ι j → κ → ℂ) (hc : ∀ j u k, ‖c j u k‖ ≤ 1)
      (alt : ∀ j, ι j → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j u k, planarProfileConstant (alt j u k) (2*P.order) ≤ P.profileBound)
      (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ) (_hv : Measurable v)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (_hg : Measurable g) (_hg1 : ∀ z, ‖g z‖ ≤ 1),
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarProfileConstant