Cutoffs.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

Smooth cylinder cutoffs, circle periodization, and regularity of covering lifts.

lemma OAI.ThreeTorus.compact_smooth_cutoff line 18

Source documentation

A compactly supported Euclidean cutoff, equal to one on a neighborhood of the prescribed compact set, not merely on the set itself.

lemma compact_smooth_cutoff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
    ∃ f : E → ℝ, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) f ∧ HasCompactSupport f ∧
      tsupport f ⊆ U ∧ (∀ x, 0 ≤ f x ∧ f x ≤ 1) ∧
      ∀ x ∈ K, f =ᶠ[𝓝 x] 1 := by
…

def OAI.ThreeTorus.cylinderPeriodize line 43
Source documentation
Periodization only in the circle coordinate.
```
def cylinderPeriodize (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ :=
…
```
lemma OAI.ThreeTorus.cylinderPeriodize_periodic line 46
lemma OAI.ThreeTorus.cylinderPeriodize_local_support line 52
lemma OAI.ThreeTorus.contDiff_cylinderPeriodize line 73
def OAI.ThreeTorus.cylinderProjection line 88
Source documentation
The covering map for the real-frequency/slow-circle cylinder.
```
def cylinderProjection (p : ℝ × ℝ) : ℝ × UnitAddCircle := (p.1,(p.2 : UnitAddCircle))
```
lemma OAI.ThreeTorus.continuous_cylinderProjection line 90
lemma OAI.ThreeTorus.cylinderProjection_surjective line 93
lemma OAI.ThreeTorus.isOpenMap_cylinderProjection line 98
lemma OAI.ThreeTorus.isQuotientMap_cylinderProjection line 101
def OAI.ThreeTorus.CylinderSmooth line 105
Source documentation
Smoothness on this cylinder is smoothness of the periodic covering lift.
```
def CylinderSmooth (f : ℝ × UnitAddCircle → ℝ) : Prop :=
…
```
lemma OAI.ThreeTorus.CylinderSmooth.continuous line 108
def OAI.ThreeTorus.cylinderCutoff line 112
Source documentation
Periodization with a smooth saturation gives a [0,1]-valued cylinder function.
```
def cylinderCutoff (f : ℝ × ℝ → ℝ) (p : ℝ × UnitAddCircle) : ℝ :=
…
```
lemma OAI.ThreeTorus.cylinderCutoff_coe line 115
lemma OAI.ThreeTorus.cylinderCutoff_smooth line 119
lemma OAI.ThreeTorus.cylinderCutoff_mem_Icc line 124
lemma OAI.ThreeTorus.cylinderPeriodize_finite line 128
lemma OAI.ThreeTorus.cylinderCutoff_one_of_eq_one line 133
lemma OAI.ThreeTorus.cylinderCutoff_support_subset line 144
lemma OAI.ThreeTorus.cylinderCutoff_tsupport_subset line 160
lemma OAI.ThreeTorus.cylinderCutoff_compactSupport line 166
lemma OAI.ThreeTorus.cylinderCutoff_one_near line 171
lemma OAI.ThreeTorus.compact_cylinder_lift line 180

theorem OAI.ThreeTorus.compact_cylinder_cutoff line 199

Source documentation

The exact smooth cutoff needed for a compact stationary image in the cylinder. The support may be placed in an arbitrary prescribed open neighborhood.

theorem compact_cylinder_cutoff {K U : Set (ℝ × UnitAddCircle)}
    (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
    ∃ χ : ℝ × UnitAddCircle → ℝ, CylinderSmooth χ ∧ HasCompactSupport χ ∧
      tsupport χ ⊆ U ∧ (∀ p, 0 ≤ χ p ∧ χ p ≤ 1) ∧
      ∀ p ∈ K, χ =ᶠ[𝓝 p] 1 := by
…

Mentions: OAI.ThreeTorus.CylinderSmooth

theorem OAI.ThreeTorus.finite_disjoint_cylinder_cutoffs line 219

Source documentation

Finite disjoint compact stationary images admit simultaneous smooth cutoffs with disjoint compact supports, in any prescribed neighborhoods.

theorem finite_disjoint_cylinder_cutoffs {ι : Type*} [Finite ι]
    (K U : ι → Set (ℝ × UnitAddCircle))
    (hK : ∀ i, IsCompact (K i)) (hU : ∀ i, IsOpen (U i))
    (hKU : ∀ i, K i ⊆ U i) (hdisj : Pairwise (Disjoint on K)) :
    ∃ χ : ι → ℝ × UnitAddCircle → ℝ,
      (∀ i, CylinderSmooth (χ i) ∧ HasCompactSupport (χ i) ∧ tsupport (χ i) ⊆ U i ∧
        (∀ p, 0 ≤ χ i p ∧ χ i p ≤ 1) ∧ ∀ p ∈ K i, χ i =ᶠ[𝓝 p] 1) ∧
      Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) := by
…

Mentions: OAI.ThreeTorus.CylinderSmooth

lemma OAI.ThreeTorus.cylinder_cutoff_finite_indices line 242

Source documentation

Compact support away from the zero frequency leaves finitely many nonzero angular indices at every positive integral scale.

lemma cylinder_cutoff_finite_indices {χ : ℝ × UnitAddCircle → ℝ}
    (hc : HasCompactSupport χ) (hzero : ∀ a, χ (0,a) = 0) (n : ℕ) (hn : 0 < n) :
    ∃ S : Finset ℤ, (0:ℤ) ∉ S ∧ ∀ j ∉ S, ∀ a, χ ((j:ℝ)/n,a) = 0 := by
…

def OAI.ThreeTorus.cylinderFirstPeriodize line 273
Source documentation
Periodization in the REAL coordinate of a compact cylinder cutoff.
```
def cylinderFirstPeriodize (χ : ℝ × UnitAddCircle → ℝ) (p : ℝ × UnitAddCircle) : ℝ :=
…
```
lemma OAI.ThreeTorus.cylinderFirstPeriodize_periodic line 276
lemma OAI.ThreeTorus.cylinderFirstPeriodize_local_support line 282
lemma OAI.ThreeTorus.cylinderFirstPeriodize_smooth line 303
def OAI.ThreeTorus.cylinderTorusCutoff line 318
Source documentation
The cutoff on the actual two-torus, not a chart-only surrogate.
```
def cylinderTorusCutoff (χ : ℝ × UnitAddCircle → ℝ) (p : UnitAddCircle × UnitAddCircle) : ℝ :=
…
```
lemma OAI.ThreeTorus.cylinderTorusCutoff_coe line 321
lemma OAI.ThreeTorus.cylinderTorusCutoff_smooth line 324
lemma OAI.ThreeTorus.cylinderTorusCutoff_continuous line 330
lemma OAI.ThreeTorus.cylinderFirstPeriodize_eq line 340
lemma OAI.ThreeTorus.cylinderTorusCutoff_eq line 358

lemma OAI.ThreeTorus.cylinder_smooth_regular line 377

Source documentation

Cover smoothness supplies the parameter-continuous first derivatives needed by stationary phase on a cylinder; it is not an additional regularity assumption on the clipped packets.

lemma cylinder_smooth_regular {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : ℝ × UnitAddCircle → E}
    (hf : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (f ∘ cylinderProjection)) :
    (∀ a, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : ℝ => f (x,a))) ∧
    Continuous f ∧ Continuous (fun p : ℝ × UnitAddCircle => deriv (fun x => f (x,p.2)) p.1) := by
…

Mentions: OAI.ThreeTorus.cylinderProjection