PassageFamilies.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

Rounded common primitives, neutral and quantile families, exact indices, signal passages, and support tracking.

lemma OAI.ThreeTorus.deriv_real_primitive line 18

theorem OAI.ThreeTorus.exists_rounded_primitive_family line 26

Source documentation

One integer-rounded primitive sequence works for every later choice of jitter. In particular the estimates for a finite list can all use exactly this sequence.

theorem exists_rounded_primitive_family {V : ℝ → ℝ}
    (hp : Periodic V 1) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) :
    ∃ Δ : ℕ → ℝ, ∃ H : ℕ → UnitAddCircle → UnitAddCircle,
      (∀ n, 0 < n → |Δ n| ≤ (n:ℝ)⁻¹) ∧ Tendsto Δ atTop (𝓝 0) ∧
      (∀ n, Continuous (H n)) ∧
      (∀ n (x : ℝ), H n (x:UnitAddCircle) =
        ((n:ℝ)*((∫ t in 0..x, V t)+Δ n*x):UnitAddCircle)) ∧
      ∀ J : ℝ → ℝ, ∀ hJp : Periodic J 1,
        ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J →
        let σ := fun (n : ℕ) (a : UnitAddCircle) => (((1+hJp.lift a/(n:ℝ))/(n:ℝ):ℝ):UnitAddCircle)
…

Mentions: OAI.ThreeTorus.H

lemma OAI.ThreeTorus.continuous_twistIter line 144
lemma OAI.ThreeTorus.two_mode_packet_correlation_zero line 149
lemma OAI.ThreeTorus.retainedPassage_pair_zero line 198
lemma OAI.ThreeTorus.finite_orthogonal_correlation line 246

theorem OAI.ThreeTorus.retained_family_spectral_moment line 288

Source documentation

Exact spectral density for a finite color list, including constant tags. Overlapping output angular indices do not cause interference: the old angular index becomes the new spare Fourier index.

theorem retained_family_spectral_moment {ι : Type*} [Fintype ι]
    {ψ : UnitAddCircle → ℝ} {χ : ι → ℝ → UnitAddCircle → ℝ}
    {m : ι → ℤ} {H : ℕ → UnitAddCircle → UnitAddCircle}
    {A : ι → UnitAddCircle × UnitAddCircle → ℂ}
    {J : UnitAddCircle → ℝ} {J₀ : ℝ → ℝ} {I : Set ℝ}
    (hψ : Continuous ψ) (hχ : ∀ i, Continuous (χ i).uncurry)
    (hH : ∀ n, Continuous (H n)) (hA : ∀ i, Continuous (A i))
    (hψs : ∀ x ∈ Ioc (0:ℝ) 1, ψ (x:UnitAddCircle) ≠ 0 → x ∈ I)
    (hj : Continuous J) (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀)
    (hJe : ∀ x ∈ I, J (x:UnitAddCircle) = J₀ x)
    (hIo : IsOpen I) (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
    (hcut : ∀ i j, i ≠ j → m i = m j → ∀ s a, χ i s a*χ j s a = 0)
…

Mentions: OAI.ThreeTorus.H

lemma OAI.ThreeTorus.sum_eq_of_zero_off line 355
lemma OAI.ThreeTorus.retainedPassage_eq_of_cover line 369
lemma OAI.ThreeTorus.exactRetainedPacketDensity_eq_of_cover line 381
lemma OAI.ThreeTorus.scalar_cutoff_stationary_one line 400
lemma OAI.ThreeTorus.core_character_support line 410
Source documentation
The actual second-passage coefficients have no spare-dependent modulus; in particular their support is controlled by the actual first core.
```
lemma core_character_support (C : ℝ → ℂ) (m : ℤ) (b : UnitAddCircle) :
    support (fun u => C u*fourier m b) ⊆ tsupport C := by
…
```

theorem OAI.ThreeTorus.cylinder_cutoff_exact_indices line 416

Source documentation

The exact finite sampling set, with no identically zero extra modes.

theorem cylinder_cutoff_exact_indices {ι : Type*}
    (χ : ι → ℝ → UnitAddCircle → ℝ)
    (hc : ∀ i, HasCompactSupport (χ i).uncurry) (hz : ∀ i a, χ i 0 a = 0) :
    ∃ S : ℕ → ι → Finset ℤ,
      (∀ n i j, j ∈ S n i → j ≠ 0) ∧
      ∀ n, 0 < n → ∀ i j, j ∈ S n i ↔ ∃ a, χ i ((j:ℝ)/n) a ≠ 0 := by
…

theorem OAI.ThreeTorus.exists_simultaneous_neutral_passage line 460

Source documentation

The jitter, all packet lists and all cutoffs are fixed before the final passage integer. No primitive, convergence, or spectral data are assumed.

theorem exists_simultaneous_neutral_passage {ι : Type*} [Fintype ι]
    {A : ι → UnitAddCircle × UnitAddCircle → ℂ} {A₀ : ι → UnitAddCircle → ℝ → ℂ}
    {V : ℝ → ℝ} {m : ι → ℤ} {o l u R : ℝ}
    (hm : ∀ i, m i ≠ 0)
    (hA : ∀ i a x, x ∈ Ioc o (o+1) → A i ((x : UnitAddCircle),a) = A₀ i a x)
    (hA₀ : ∀ i a, ContDiff ℝ 2 (A₀ i a)) (hAc : ∀ i, Continuous (A₀ i).uncurry)
    (hAd : ∀ i, Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ i p.1) p.2))
    (hAr : ∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun p : ℝ × ℝ => A₀ i (p.2 : UnitAddCircle) p.1))
    (hsupp : ∀ i a, support (A₀ i a) ⊆ Ioc l u)
    (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u) (hR : 0 < R)
    (hp : Periodic V 1) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
…

def OAI.ThreeTorus.retainedRealCore line 574
def OAI.ThreeTorus.retainedRealAmplitude line 579
lemma OAI.ThreeTorus.retainedRealCore_smooth line 585
lemma OAI.ThreeTorus.retainedRealAmplitude_support line 599

lemma OAI.ThreeTorus.retainedRealAmplitude_regular line 608

Source documentation

Every analytic lift condition required by the next stationary-phase passage follows from the smooth real core and the spare character.

lemma retainedRealAmplitude_regular {C : ℝ → ℂ}
    (hC : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) C) (m : ℤ) :
    (∀ b : UnitAddCircle, ContDiff ℝ 2 (fun u : ℝ => C u*fourier m b)) ∧
    Continuous (fun p : UnitAddCircle × ℝ => C p.2*fourier m p.1) ∧
    Continuous (fun p : UnitAddCircle × ℝ => deriv (fun u : ℝ => C u*fourier m p.1) p.2) ∧
    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun p : ℝ × ℝ => C p.1*fourier m (p.2:UnitAddCircle)) := by
…

lemma OAI.ThreeTorus.retainedRealAmplitude_matches line 625
lemma OAI.ThreeTorus.retainedAmplitude_smooth_lift line 635
lemma OAI.ThreeTorus.retainedRealCore_tsupport_subset line 658
lemma OAI.ThreeTorus.retainedRealCore_tsupport_cylinder line 668
lemma OAI.ThreeTorus.retainedRealCore_disjoint line 680

lemma OAI.ThreeTorus.compact_inside_buffered_interval line 692

Source documentation

The buffered real integration interval can always be fixed before the next passage integer, even when all the coefficients are zero.

lemma compact_inside_buffered_interval {K : Set ℝ} {a b : ℝ}
    (hK : IsCompact K) (hab : a < b) (hKI : K ⊆ Ioo a b) :
    ∃ l u R : ℝ, a < l ∧ l < u ∧ u < b ∧ 0 < R ∧
      K ⊆ Ioc l u ∧ Icc (l-2*R) (u+2*R) ⊆ Ioo a b := by
…

abbrev OAI.ThreeTorus.PassageOutputIndex line 751
def OAI.ThreeTorus.passageOutputCore line 753
lemma OAI.ThreeTorus.passageOutputCore_disjoint line 759

theorem OAI.ThreeTorus.second_separation_of_actual_output line 784

Source documentation

After the first finite passage integer is fixed, a single integral carrier and a family of smooth scalar-only cutoffs give the second passage exactly disjoint final angular index sets. These cutoffs are one near the stationary images of the actual first output supports.

theorem second_separation_of_actual_output {ι : Type*} [Fintype ι]
    (S : ι → Finset ℤ) (ψ₀ : ℝ → ℝ) (χ : ι → ℝ → UnitAddCircle → ℝ)
    (m : ι → ℤ) (H : UnitAddCircle → UnitAddCircle)
    (A : ι → UnitAddCircle × UnitAddCircle → ℂ) (n : ℕ)
    (hS : ∀ i j, j ∈ S i → j ≠ 0)
    (hψ : HasCompactSupport ψ₀) (I : Set ℝ) (hψI : tsupport ψ₀ ⊆ I)
    (hχd : Pairwise (fun i j => Disjoint (tsupport (χ i).uncurry) (tsupport (χ j).uncurry)))
    (φ : UnitAddCircle → ℝ) (hφ : Continuous φ)
    (hi : InjOn (fun u : ℝ => φ (u:UnitAddCircle)) I) :
    ∃ c : ℕ, 0 < c ∧
      (∀ u : ℝ, (c:ℝ)+φ (u:UnitAddCircle) ≠ 0) ∧
      ∃ (ξ : PassageOutputIndex S → ℝ → ℝ) (T : ℕ → PassageOutputIndex S → Finset ℤ),
…

Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.PassageOutputIndex

structure OAI.ThreeTorus.PassagePackets line 854
Source documentation
All input data used by the proved simultaneous passage theorems. No asymptotic estimate, transport, density, or conclusion is a field.
```
structure PassagePackets (ι : Type*) where
…
```
def OAI.ThreeTorus.PassagePackets.SpareIndependent line 882
lemma OAI.ThreeTorus.smooth_new_speed line 886
lemma OAI.ThreeTorus.positive_deriv_new_speed line 891

theorem OAI.ThreeTorus.literal_output_packets line 901

Source documentation

A neutral or quantile passage produces a valid input family for the next passage, with all real lifts supported in one common compact good interval. The jitter may be arbitrarily broad. The constructor works at EVERY positive passage integer, independently of the spectral/physical approximation bounds.

theorem literal_output_packets {ι : Type*} [Fintype ι]
    (m : ι → ℤ) (A : ι → UnitAddCircle × UnitAddCircle → ℂ)
    (H : ℕ → UnitAddCircle → UnitAddCircle) (Hl : ℕ → ℝ → ℝ)
    (χ : ι → ℝ → UnitAddCircle → ℝ) (S : ι → Finset ℤ)
    (hS : ∀ i j, j ∈ S i → j ≠ 0)
    (hAc : ∀ i, Continuous (A i))
    (hAs : ∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ => A i (p.1,p.2)))
    (hχ : ∀ i, CylinderSmooth (χ i).uncurry) (hχc : ∀ i, Continuous (χ i).uncurry)
    (hHc : ∀ n, Continuous (H n))
    (hHl : ∀ n, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (Hl n))
    (hHe : ∀ n (x : ℝ), H n (x:UnitAddCircle) = (Hl n x:UnitAddCircle))
    {δ : ℝ} (c : LawCutoffs δ) (hδ : 0 < δ) (hδ' : δ < 1/8)
…

Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.LawCutoffs

lemma OAI.ThreeTorus.output_index_injective line 978
theorem OAI.ThreeTorus.exists_simultaneous_quantile_passage line 1007
theorem OAI.ThreeTorus.exists_signal_family_law line 1124

theorem OAI.ThreeTorus.eventually_integral_speed_separation line 1179

Source documentation

The integral carrier can meet every additional lower bound, as required when the signal strength and approximation tolerance are selected first.

theorem eventually_integral_speed_separation {ι X : Type*} [Finite ι]
    [TopologicalSpace X] [CompactSpace X] (m : ι → ℤ) (φ : X → ℝ)
    (hm : ∀ i, m i ≠ 0) (hφ : Continuous φ) :
    ∀ᶠ c : ℕ in Filter.atTop, 0 < c ∧
      (∀ i x, (m i : ℝ) * ((c:ℝ) + φ x) ≠ 0) ∧
      (∀ i j x y, (m i : ℝ) * ((c:ℝ) + φ x) =
        (m j : ℝ) * ((c:ℝ) + φ y) → m i = m j) := by
…

def OAI.ThreeTorus.ActualQuantileFamily line 1242

Source documentation

The full conclusion of the actual quantile passage. This abbreviation contains geometry, exact Fourier coefficients, all moments, and both errors; its constructor below assumes no one of these output conclusions.

def ActualQuantileFamily {ι : Type*}
    (A : ι → UnitAddCircle × UnitAddCircle → ℂ)
    (A₀ : ι → UnitAddCircle → ℝ → ℂ) (V : ℝ → ℝ) (m : ι → ℤ)
    (l u R : ℝ) (ρ : ℝ → ℝ) {δ : ℝ} (c : LawCutoffs δ)
    (χ : ι → ℝ → UnitAddCircle → ℝ) (g : ι → UnitAddCircle → ℝ) (ε : ℝ) : Prop :=
…

Mentions: OAI.ThreeTorus.LawCutoffs

theorem OAI.ThreeTorus.exists_actual_signal_family line 1290

theorem OAI.ThreeTorus.tracked_frequency_cutoffs line 1386

Source documentation

Scalar cutoffs with an arbitrarily small stationary-image enlargement, exactly disjoint angular ranges, and the required identity on the true weights.

theorem tracked_frequency_cutoffs {ι : Type*} [Finite ι]
    (m : ι → ℤ) (V : ℝ → ℝ) (K : ι → Set ℝ)
    (hV : Continuous V) (hK : ∀ i, IsCompact (K i))
    (h0 : ∀ i, 0 ∉ (fun x => (m i:ℝ)*V x) '' K i)
    (hsep : Pairwise (fun i j => Disjoint ((fun x => (m i:ℝ)*V x) '' K i)
      ((fun x => (m j:ℝ)*V x) '' K j)))
    {η : ℝ} (hη : 0 < η) :
    ∃ χ : ι → ℝ → ℝ,
      (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (χ i) ∧ HasCompactSupport (χ i) ∧
        χ i 0 = 0 ∧ (∀ s, 0 ≤ χ i s ∧ χ i s ≤ 1) ∧
        (∀ s ∈ (fun x => (m i:ℝ)*V x) '' K i, χ i =ᶠ[𝓝 s] 1) ∧
        (∀ s ∈ tsupport (χ i), ∃ x ∈ K i, |s-(m i:ℝ)*V x| < η) ∧
…

lemma OAI.ThreeTorus.circle_dist_le_real line 1418
lemma OAI.ThreeTorus.integral_carrier_circle line 1423

lemma OAI.ThreeTorus.passage_temporal_drift line 1433

Source documentation

The temporal displacement uses the SAME old support point as the index location. A large jitter changes only the final lower bound on n.

lemma passage_temporal_drift {s v J η : ℝ} {m c : ℤ} {n : ℕ}
    (hn : 0 < n) (hs : |s-(m:ℝ)*((c:ℝ)+v)| ≤ η) :
    dist ((s+s*J/n:ℝ):UnitAddCircle) ((m:ℝ)*v:UnitAddCircle) ≤
      η+|s| *|J|/n := by
…

lemma OAI.ThreeTorus.passage_index_drift line 1446
lemma OAI.ThreeTorus.passage_retained_size line 1465