Transmission.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Law averaging and weighted errors, folded packet transmission, and concrete signal-circle comparison.

lemma OAI.ThreeTorus.continuousAt_scaled_periodization_compact line 33
Source documentation
Compactly supported realized laws have a locally finite scaled lattice sum, jointly in the nonzero scale and the unfolded circle coordinate.
```
lemma continuousAt_scaled_periodization_compact {q : ℝ → ℝ} (hq : Continuous q)
    (hc : HasCompactSupport q) {p : ℝ × ℝ} (hp : p.1 ≠ 0) :
    ContinuousAt (fun v : ℝ × ℝ => periodizedReal (scaledDensity q v.1) v.2) p := by
…
```
Mentions: OAI.ThreeTorus.periodizedReal, OAI.ThreeTorus.scaledDensity

lemma OAI.ThreeTorus.continuousAt_scaled_periodization_bandlimited line 80

Source documentation

Compact bandwidth gives local joint continuity of the ideal law's folded density.

lemma continuousAt_scaled_periodization_bandlimited {q : ℝ → ℝ} (hq : Continuous q)
    (hqi : Integrable q) {C : ℝ} (hC : 0 ≤ C) (hb : ∀ y, |q y| ≤ C/(1+y^2))
    {D : ℝ} (hF : ∀ v, D < |v| → 𝓕 (fun y => (q y : ℂ)) v = 0)
    {p : ℝ × ℝ} (hp : p.1 ≠ 0) :
    ContinuousAt (fun v : ℝ × ℝ => periodizedReal (scaledDensity q v.1) v.2) p := by
…

Mentions: OAI.ThreeTorus.periodizedReal, OAI.ThreeTorus.scaledDensity

lemma OAI.ThreeTorus.continuous_weighted_fold_difference line 116

lemma OAI.ThreeTorus.scaled_fold_l1_difference line 143

Source documentation

Scaling and folding are contractions for the total variation distance of real densities, including subprobability densities and negative scales.

lemma scaled_fold_l1_difference {q r : ℝ → ℝ} (hqm : Measurable q) (hqi : Integrable q)
    (hrm : Measurable r) (hri : Integrable r) {s : ℝ} (hs : s ≠ 0) :
    (∫ y, |foldCircleDensity (scaledDensity q s) y-foldCircleDensity (scaledDensity r s) y|
      ∂AddCircle.haarAddCircle) ≤ ∫ x, |q x-r x| := by
…

Mentions: OAI.ThreeTorus.foldCircleDensity, OAI.ThreeTorus.scaledDensity

theorem OAI.ThreeTorus.weighted_fold_law_average line 160

Source documentation

Exact fast law comparison, with the missing mass of the realized subprobability included. All arbitrary offsets are allowed.

theorem weighted_fold_law_average {w q r : ℝ → ℝ}
    (hw : Continuous w) (hwc : HasCompactSupport w) (hw0 : 0 ∉ tsupport w)
    (hwn : ∀ s, 0 ≤ w s)
    (hq : Continuous q) (hqc : HasCompactSupport q)
    (hr : Continuous r) (hri : Integrable r) {C : ℝ} (hC : 0 ≤ C)
    (hb : ∀ y, |r y| ≤ C/(1+y^2)) {D : ℝ}
    (hF : ∀ v, D < |v| → 𝓕 (fun y => (r y : ℂ)) v = 0)
    (β : ℕ → UnitAddCircle) :
    Tendsto (fun n : ℕ => ∫ s, w s *
      |foldCircleDensity (scaledDensity q s) ((((n:ℝ)*s:ℝ):UnitAddCircle)+β n)-
        foldCircleDensity (scaledDensity r s) ((((n:ℝ)*s:ℝ):UnitAddCircle)+β n)|) atTop
      (𝓝 (∫ s, w s * ∫ y,
…

Mentions: OAI.ThreeTorus.foldCircleDensity, OAI.ThreeTorus.scaledDensity

lemma OAI.ThreeTorus.continuous_weighted_fold_of_local line 211
lemma OAI.ThreeTorus.continuous_weighted_fold_compact line 230
lemma OAI.ThreeTorus.continuous_weighted_fold_bandlimited line 235
lemma OAI.ThreeTorus.continuous_fast_circle line 243
lemma OAI.ThreeTorus.continuous_weighted_fast_compact line 247
lemma OAI.ThreeTorus.foldCircleDensity_mul_circle line 255
lemma OAI.ThreeTorus.fast_circle_coe line 260
lemma OAI.ThreeTorus.foldCircleDensity_mul_fast line 265

theorem OAI.ThreeTorus.realized_fold_signal_estimate line 274

Source documentation

Quantitative transfer from an ideal folded law to a realized compact law. The phase may have any prescribed offset at every passage integer.

theorem realized_fold_signal_estimate {w q r : ℝ → ℝ}
    (hw : Continuous w) (hwc : HasCompactSupport w) (hw0 : 0 ∉ tsupport w)
    (hwn : ∀ s, 0 ≤ w s)
    (hq : Continuous q) (hqc : HasCompactSupport q)
    (hr : Continuous r) (hri : Integrable r) {C : ℝ} (hC : 0 ≤ C)
    (hb : ∀ y, |r y| ≤ C/(1+y^2)) {D : ℝ}
    (hF : ∀ v, D < |v| → 𝓕 (fun y => (r y : ℂ)) v = 0)
    {g : UnitAddCircle → ℝ} (hg : Continuous g) {ε : ℝ}
    (hideal : ∀ s ∈ support w, ∀ y, |foldCircleDensity (scaledDensity r s) y-g y| ≤ ε)
    (β : ℕ → UnitAddCircle) {η : ℝ} (hη : 0 < η) :
    ∀ᶠ n : ℕ in atTop, (∫ z,
      |foldCircleDensity (fun s => w s*foldCircleDensity (scaledDensity q s)
…

Mentions: OAI.ThreeTorus.foldCircleDensity, OAI.ThreeTorus.scaledDensity

lemma OAI.ThreeTorus.lawJitter_injOn line 336

lemma OAI.ThreeTorus.lawJitter_branchKernel line 348

Source documentation

The inverse-branch Jacobian is exactly the realized quantile density, not merely some density representing the same measure.

lemma lawJitter_branchKernel {ρ : ℝ → ℝ} {δ : ℝ} (c : LawCutoffs δ)
    (hρ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ρ) (hi : Integrable ρ)
    (hp : ∀ y, 0 < ρ y) (hm : ∫ y, ρ y = 1) (hδ : 0 < δ)
    (w : ℝ → ℝ) (y s : ℝ) :
    branchKernel (Ioo δ (1-δ)) (lawJitter ρ c) (fun p : ℝ × ℝ => w p.2*c.ψ p.1^2) (y,s) =
      w s*lawDensity ρ c y := by
…

Mentions: OAI.ThreeTorus.LawCutoffs, OAI.ThreeTorus.branchKernel, OAI.ThreeTorus.lawJitter, OAI.ThreeTorus.lawDensity

lemma OAI.ThreeTorus.lawJitter_passageKernel line 379
lemma OAI.ThreeTorus.lawJitter_fineKernel line 390
lemma OAI.ThreeTorus.stationaryWeight_modulus_independent line 403
lemma OAI.ThreeTorus.stationaryCutoffLift_modulus_independent line 411
lemma OAI.ThreeTorus.stationaryWeight_nonneg line 425
lemma OAI.ThreeTorus.stationaryWeight_tsupport_subset line 432
lemma OAI.ThreeTorus.stationaryWeight_slice_regular line 437

theorem OAI.ThreeTorus.quantile_fine_signal_estimate line 455

Source documentation

Fully realized smooth quantile law: the exact branch kernel has the desired signal, with both its missing mass and total variation error explicitly included.

theorem quantile_fine_signal_estimate {w ρ : ℝ → ℝ}
    (hw : Continuous w) (hwc : HasCompactSupport w) (hw0 : 0 ∉ tsupport w)
    (hwn : ∀ s, 0 ≤ w s)
    (hρ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ρ) (hi : Integrable ρ)
    (hp : ∀ y, 0 < ρ y) (hm : ∫ y, ρ y = 1)
    {C : ℝ} (hC : 0 ≤ C) (hb : ∀ y, |ρ y| ≤ C/(1+y^2)) {D : ℝ}
    (hF : ∀ v, D < |v| → 𝓕 (fun y => (ρ y : ℂ)) v = 0)
    {δ : ℝ} (c : LawCutoffs δ) (hδ : 0 < δ) (hδ' : δ < 1/8)
    {g : UnitAddCircle → ℝ} (hg : Continuous g) {ε : ℝ}
    (hideal : ∀ s ∈ support w, ∀ y, |foldCircleDensity (scaledDensity ρ s) y-g y| ≤ ε)
    {η : ℝ} (hη : 0 < η) :
    ∀ᶠ n : ℕ in atTop, (∫ z,
…

Mentions: OAI.ThreeTorus.LawCutoffs, OAI.ThreeTorus.foldCircleDensity, OAI.ThreeTorus.scaledDensity

def OAI.ThreeTorus.quantileCircleJitter line 494
lemma OAI.ThreeTorus.quantileCircleJitter_coe line 497
lemma OAI.ThreeTorus.continuous_quantileCircleJitter line 500

def OAI.ThreeTorus.exactRetainedPacketDensity line 507

Source documentation

The finite retained spectral density of one actual signed Fourier packet.

def exactRetainedPacketDensity (I : Set ℝ) (J₀ : ℝ → ℝ) (ψ : UnitAddCircle → ℝ)
    (χ : ℝ → UnitAddCircle → ℝ) (m : ℤ) (H : ℕ → UnitAddCircle → UnitAddCircle)
    (A : UnitAddCircle × UnitAddCircle → ℂ) (S : Finset ℤ) (n : ℕ) : UnitAddCircle → ℝ :=
…

Mentions: OAI.ThreeTorus.H

lemma OAI.ThreeTorus.exactRetainedPacketDensity_integrable line 515
lemma OAI.ThreeTorus.integral_abs_sub_triangle line 531

theorem OAI.ThreeTorus.exact_quantile_circle_spectral_estimate line 544

Source documentation

Source transmission analytic assembly, for the actual retained signed coefficients and actual smooth quantile jitter. The law's lost mass is counted. The model bound has to be established for the ideal law; no passage limit is assumed. Every sufficiently large integer works.

theorem exact_quantile_circle_spectral_estimate
    {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
    {Pr V : ℝ → ℝ} {m : ℤ} {Δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
    {o l u R : ℝ}
    (hm : m ≠ 0)
    (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(Pr x+Δ n*x) : UnitAddCircle))
    (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
    (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
    (hAd : Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ p.1) p.2))
    (hAr : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun p : ℝ × ℝ => A₀ (p.2 : UnitAddCircle) p.1))
    (hsupp : ∀ a, support (A₀ a) ⊆ Ioc l u)
…

Mentions: OAI.ThreeTorus.H

def OAI.ThreeTorus.signalCircleModel line 658
Source documentation
The exact three-mode index signal, in the source's positive-moment convention.
```
noncomputable def signalCircleModel (P : ℕ) (γ B : ℝ) (d : ℝ → ℂ) (m : ℤ) (z : UnitAddCircle) : ℝ := by
…
```
lemma OAI.ThreeTorus.continuous_signalCircleModel line 662
lemma OAI.ThreeTorus.signalCircleModel_uniform_on_weight line 667

lemma OAI.ThreeTorus.signalJitter_law_regular line 703

Source documentation

All the analytic prerequisites of the actual signal law, including mass one, are consequences of the explicit positive joint law.

lemma signalJitter_law_regular {α B c D γ : ℝ}
    (hα : 0 < α) (hB : 0 < B) (hc : 0 < c) (hαD : α ≤ D)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hcomp : HasCompactSupport d) (hr : ∀ v, d (-v) = starRingEnd ℂ (d v))
    (h0 : d 0 = 0) (hs : Function.support d ⊆ Icc (-D) D) (P : ℕ) [NeZero P]
    (hbound : ∀ h R, signalBaseline α R/(2*P) ≤ signalJoint α γ d P h R ∧
      signalJoint α γ d P h R ≤ 3*signalBaseline α R/(2*P)) :
    let ρ := signalJitter α γ d P B c
…

Mentions: OAI.ThreeTorus.signalBaseline, OAI.ThreeTorus.signalJoint, OAI.ThreeTorus.signalJitter