Twists.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Product torus, exact angular packets, all integer twist iterates, and measure-preserving passage charts.

abbrev OAI.ThreeTorus.TripleTorus line 16
abbrev OAI.ThreeTorus.slowVolume line 17
abbrev OAI.ThreeTorus.tripleVolume line 19
def OAI.ThreeTorus.packet line 22
Source documentation
The actual angular packet, in the volume preserving coordinates of section 2.
```
def packet (m : ℤ) (A : UnitAddCircle × UnitAddCircle → ℂ) (x : TripleTorus) : ℂ :=
…
```
Mentions: OAI.ThreeTorus.TripleTorus
def OAI.ThreeTorus.twistIter line 26
Source documentation
All integer powers of an intermediate twist in its coordinates.
```
def twistIter (φ : UnitAddCircle → UnitAddCircle) (n : ℤ) (x : TripleTorus) : TripleTorus :=
…
```
Mentions: OAI.ThreeTorus.TripleTorus
lemma OAI.ThreeTorus.twistIter_add line 29
lemma OAI.ThreeTorus.fourier_zsmul line 36
lemma OAI.ThreeTorus.packet_twistIter line 40
lemma OAI.ThreeTorus.continuous_packet line 49
lemma OAI.ThreeTorus.integral_fourier_pair line 53

lemma OAI.ThreeTorus.integral_packet_pair line 61

Source documentation

Exact packet orthogonality, before stationary phase or any passage limit.

lemma integral_packet_pair {A B : UnitAddCircle × UnitAddCircle → ℂ}
    (hA : Continuous A) (hB : Continuous B) (m k : ℤ) :
    (∫ x : TripleTorus, starRingEnd ℂ (packet m A x)*packet k B x ∂tripleVolume) =
      if m = k then ∫ ua, starRingEnd ℂ (A ua)*B ua ∂slowVolume else 0 := by
…

Mentions: OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.packet, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.slowVolume

lemma OAI.ThreeTorus.normSq_complex line 83

lemma OAI.ThreeTorus.packet_correlation line 87

Source documentation

Exact correlation formula for a packet under every positive or negative power.

lemma packet_correlation {A : UnitAddCircle × UnitAddCircle → ℂ}
    (hA : Continuous A) {φ : UnitAddCircle → UnitAddCircle} (hφ : Continuous φ)
    (m n : ℤ) :
    (∫ x : TripleTorus, starRingEnd ℂ (packet m A x)*
      packet m A (twistIter φ n x) ∂tripleVolume) =
    ∫ ua : UnitAddCircle × UnitAddCircle,
      fourier n (m • φ ua.1)*(‖A ua‖^2 : ℝ) ∂slowVolume := by
…

Mentions: OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.packet, OAI.ThreeTorus.twistIter, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.slowVolume

def OAI.ThreeTorus.packetSpectralMeasure line 112

Source documentation

Packet spectral measure is the precise pushforward stated in (2.3).

def packetSpectralMeasure (φ : UnitAddCircle → UnitAddCircle) (m : ℤ)
    (A : UnitAddCircle × UnitAddCircle → ℂ) : Measure UnitAddCircle :=
…

lemma OAI.ThreeTorus.packet_spectral_moment line 117
lemma OAI.ThreeTorus.continuous_fourier_parseval line 133

lemma OAI.ThreeTorus.Fourier_cutoff_error line 146

Source documentation

Exact Parseval identity for arbitrary finite smooth coefficient cutoffs.

lemma Fourier_cutoff_error {f : UnitAddCircle → ℂ} (hf : Continuous f)
    (S : Finset ℤ) (χ : ℤ → ℂ) :
    (∫ θ : UnitAddCircle,
      ‖f θ-∑ j ∈ S, χ j*fourierCoeff f j*fourier j θ‖^2 ∂AddCircle.haarAddCircle) =
    ∑' j : ℤ, ‖(1-(if j ∈ S then χ j else 0))*fourierCoeff f j‖^2 := by
…

lemma OAI.ThreeTorus.cutoff_normSq_le_mass_error line 207
Source documentation
The exact cutoff energy is bounded by coefficient-mass error; the model mass need not be a Fourier coefficient of any function.
```
lemma cutoff_normSq_le_mass_error {c : ℂ} {χ w : ℝ}
    (hχ : 0 ≤ χ ∧ χ ≤ 1) (hw : w ≠ 0 → χ = 1) :
    ‖(1-(χ:ℂ))*c‖^2 ≤ |‖c‖^2-w| := by
…
```
lemma OAI.ThreeTorus.Fourier_cutoff_le_mass_error line 222

lemma OAI.ThreeTorus.integrable_nonneg_tsum line 244

Source documentation

Tonelli in real form for a summable nonnegative array.

lemma integrable_nonneg_tsum {Ω ι : Type*} [MeasurableSpace Ω] [Countable ι]
    {μ : Measure Ω} {E : ι → Ω → ℝ} (hE : ∀ j, Integrable (E j) μ)
    (h0 : ∀ j a, 0 ≤ E j a) (hp : ∀ᵐ a ∂μ, Summable (fun j => E j a))
    (hs : Summable (fun j => ∫ a, E j a ∂μ)) :
    Integrable (fun a => ∑' j, E j a) μ := by
…

Mentions: OAI.ThreeTorus.μ

lemma OAI.ThreeTorus.integrated_Fourier_cutoff_le_mass_error line 269

Source documentation

Integrating the genuine Fourier reconstruction error preserves the summed stationary mass bound from (2.14), with no assertion of an L² leading phase.

lemma integrated_Fourier_cutoff_le_mass_error {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {f : Ω → UnitAddCircle → ℂ} (hf : ∀ a, Continuous (f a))
    (S : Finset ℤ) (χ W : ℤ → Ω → ℝ)
    (hχ : ∀ j a, 0 ≤ χ j a ∧ χ j a ≤ 1)
    (hW : ∀ j a, W j a ≠ 0 → j ∈ S ∧ χ j a = 1)
    (hE : ∀ j, Integrable (fun a => |‖fourierCoeff (f a) j‖^2-W j a|) μ)
    (hp : ∀ᵐ a ∂μ, Summable (fun j => |‖fourierCoeff (f a) j‖^2-W j a|))
    (hs : Summable (fun j => ∫ a, |‖fourierCoeff (f a) j‖^2-W j a| ∂μ)) :
    (∫ a, ∫ θ : UnitAddCircle,
      ‖f a θ-∑ j ∈ S, (χ j a:ℂ)*fourierCoeff (f a) j*fourier j θ‖^2
        ∂AddCircle.haarAddCircle ∂μ) ≤
      ∑' j : ℤ, ∫ a, |‖fourierCoeff (f a) j‖^2-W j a| ∂μ := by
…

Mentions: OAI.ThreeTorus.μ

def OAI.ThreeTorus.circleCycle line 293
def OAI.ThreeTorus.circleThetaShear line 299
def OAI.ThreeTorus.passageChart line 305
def OAI.ThreeTorus.passageTwist line 308
def OAI.ThreeTorus.passageMap line 311
lemma OAI.ThreeTorus.passage_conjugacy line 321
lemma OAI.ThreeTorus.measurePreserving_circleCycle line 327
lemma OAI.ThreeTorus.measurePreserving_fiberTranslate line 332
lemma OAI.ThreeTorus.measurePreserving_circleThetaShear line 339
lemma OAI.ThreeTorus.measurePreserving_passageChart line 345
lemma OAI.ThreeTorus.passageChart_inverse_measurable line 349
lemma OAI.ThreeTorus.measurePreserving_passageChart_inverse line 355
lemma OAI.ThreeTorus.passage_as_conjugate line 363
lemma OAI.ThreeTorus.measurePreserving_passageMap line 371