OAI/Analysis/LipschitzHilbert/Trees/SourceCenteredMaskedVariation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Symmetric frozen coefficients in the actual masked synthesis. The exact three-cutoff identity gives a fixed three-event loss, with no assumption about the measure of selector boundary sets.

  1. def OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedBand line 25
  2. def OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedVariation line 31
  3. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedBand_continuous line 35
  4. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedVariation_continuous line 47
  5. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedBand_eq line 59
  6. theorem OAI.LipschitzHilbert.SourceLatticePacket.partial_add_sub line 76
  7. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedPartial_eq line 86
  8. theorem OAI.LipschitzHilbert.SourceLatticePacket.cubic_variation_add_sub_le line 101
  9. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedVariation_le line 113
  10. theorem OAI.LipschitzHilbert.SourceLatticePacket.physical_centered_masked_variation_tail line 126

    Source documentation

    The fixed three-cutoff loss costs one extra polynomial power and one unit in the exponential rate.

    theorem physical_centered_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