OAI/Analysis/LipschitzHilbert/Trees/SourceMaskMotion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual top mask preserves interval motion. Only absolute mask differences occur, so no nonvanishing hypothesis is imposed on the mask.

  1. def OAI.LipschitzHilbert.diagonalModulationIsometry line 18

    Source documentation

    The common diagonal carrier as a complex linear isometry.

    def diagonalModulationIsometry (frequency : κ → ℝ) (t : ℝ) :
    EuclideanSpace ℂ κ →ₗᵢ[ℂ] EuclideanSpace ℂ κ where
…
  2. theorem OAI.LipschitzHilbert.diagonalModulationIsometry_apply line 33
  3. def OAI.LipschitzHilbert.diagonalModulationRealIsometry line 37
  4. theorem OAI.LipschitzHilbert.diagonalModulationRealIsometry_apply line 43
  5. theorem OAI.LipschitzHilbert.masked_isometry_motion line 47
  6. theorem OAI.LipschitzHilbert.SlopeBox.mask_slope_coordinates_motion line 68
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval_coeff_smul line 83
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_labeled_masked_interval_motion line 95

    Source documentation

    Original physical coefficients, the original top carrier, and the mask evaluated at each endpoint. The only pointwise estimate used is the already established interval concentration on the snapshot vertical line.

    theorem source_labeled_masked_interval_motion (p : ℝ) (D B : ℕ) :
    ∃ L0 : ℝ, 1 ≤ L0 ∧ (B : ℝ) ≤ L0 ∧ ∀ L : ℝ, L0 ≤ L →
      ∀ (N : ℕ) (κ : Type) (Label : Fin N → Type) (Item : ∀ j, Label j → Type)
        [Fintype κ] [∀ j l, Fintype (Item j l)]
        (P : SourceLabeledLattice N κ Label Item)
        (_hcard : ∀ j, (P.labels j).card ≤ B), P.constant ≤ L^p →
      ∀ (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ × ℝ) ℂ)
        (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
        (T : SlopeBox) (K : ℝ), 1 ≤ K → SourceLabeledTopGeometry P T K D →
      ∀ (cutoff : Fin N → ℝ) (v : ℝ × ℝ → ℝ), Measurable v →
      ∀ (g : ℝ × ℝ → EuclideanSpace ℂ κ), Measurable g → (∀ z, ‖g z‖ ≤ 1) →
      ∀ (lower upper : ℕ), lower ≤ upper → ∀ r : ℝ, 0 < r →
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledTopGeometry