OAI/Dynamics/ThreeTorus/Prediction.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Laurent prediction, flat packet filling, color energies, measurable packets, reflected smoothing, and prepared pairs.

  1. lemma OAI.ThreeTorus.memLp_multiplyPackets line 17
  2. lemma OAI.ThreeTorus.multiplyPackets_energy_flat line 27
  3. lemma OAI.ThreeTorus.multiplyPackets_sub line 42
  4. lemma OAI.ThreeTorus.multiplyPackets_distance_flat line 49
  5. def OAI.ThreeTorus.finitePacketLaurent line 62

    Source documentation

    A literal finite Laurent polynomial in the Koopman orbit of a measurable packet vector.

    def finitePacketLaurent (φ : UnitAddCircle → UnitAddCircle) (m : ι → ℤ)
    (A : ι → UnitAddCircle × UnitAddCircle → ℂ) (c : ℤ →₀ ℂ) (x : TripleTorus) : ℂ :=
…

    Mentions: OAI.ThreeTorus.TripleTorus

  6. lemma OAI.ThreeTorus.finitePacketLaurent_eq_multiplier line 67
  7. lemma OAI.ThreeTorus.exists_finitePacketLaurent_approx line 81
  8. lemma OAI.ThreeTorus.multiplyPackets_whiten_reconstruct_ae line 123
  9. lemma OAI.ThreeTorus.exists_whitened_laurent_approx line 139
  10. lemma OAI.ThreeTorus.whitenPackets_distance_mass line 167
  11. lemma OAI.ThreeTorus.exists_integer_period_subinterval_above line 207
  12. lemma OAI.ThreeTorus.exists_flat_packet_spectra_above line 233
  13. def OAI.ThreeTorus.paddedAngular line 297
  14. def OAI.ThreeTorus.paddedOld line 300
  15. def OAI.ThreeTorus.paddedFlat line 303
  16. lemma OAI.ThreeTorus.paddedAngular_injective line 307
  17. lemma OAI.ThreeTorus.finitePacketVector_paddedOld line 331
  18. lemma OAI.ThreeTorus.finitePacketSpectralMeasure_paddedOld line 337
  19. lemma OAI.ThreeTorus.finitePacketSpectralMeasure_paddedFlat line 349
  20. lemma OAI.ThreeTorus.ColoredState.density_smooth line 379
  21. def OAI.ThreeTorus.ColoredState.totalVector line 386
  22. lemma OAI.ThreeTorus.ColoredState.totalVector_eq line 387
  23. lemma OAI.ThreeTorus.ColoredState.totalDensity_eq line 393
  24. lemma OAI.ThreeTorus.ColoredState.totalVector_continuous line 399
  25. lemma OAI.ThreeTorus.ColoredState.totalVector_spectral_moment line 402
  26. lemma OAI.ThreeTorus.ColoredState.total_mass_energy line 419
  27. lemma OAI.ThreeTorus.ColoredState.exists_center line 432
  28. structure OAI.ThreeTorus.MeasurablePackets line 458
  29. def OAI.ThreeTorus.MeasurablePackets.vector line 471
  30. def OAI.ThreeTorus.MeasurablePackets.spectrum line 472
  31. def OAI.ThreeTorus.MeasurablePackets.Reflection line 475
  32. def OAI.ThreeTorus.MeasurablePackets.Supported line 478
  33. lemma OAI.ThreeTorus.MeasurablePackets.vector_memLp line 481
  34. lemma OAI.ThreeTorus.MeasurablePackets.vector_centered line 482
  35. lemma OAI.ThreeTorus.MeasurablePackets.vector_real line 484
  36. lemma OAI.ThreeTorus.MeasurablePackets.spectrum_eq line 486
  37. lemma OAI.ThreeTorus.MeasurablePackets.flat_moment line 491
  38. def OAI.ThreeTorus.ColoredState.measurablePackets line 503
  39. lemma OAI.ThreeTorus.ColoredState.measurablePackets_vector line 513
  40. lemma OAI.ThreeTorus.ColoredState.measurablePackets_spectrum line 517
  41. lemma OAI.ThreeTorus.ColoredState.totalDensity_even line 533
  42. lemma OAI.ThreeTorus.exists_reflected_slow_approx line 555

    Source documentation

    Approximation is chosen on the positive members only; the negative members are their literal conjugates. Thus reality is exact, not merely AE.

    lemma exists_reflected_slow_approx (F : MeasurablePackets)
    {τ : F.Index → F.Index} (hr : F.Reflection τ) {ε : ℝ} (hε : 0 < ε) :
    ∃ g : F.Index → UnitAddCircle × UnitAddCircle → ℂ,
      (∀ i, Continuous (g i)) ∧
      (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ => g i (p.1,p.2))) ∧
      (∀ i p, g (τ i) p = conj (g i p)) ∧
      ∀ i, eLpNorm (fun p => F.A i p-g i p) 2 slowVolume < ENNReal.ofReal ε := by
…

    Mentions: OAI.ThreeTorus.MeasurablePackets, OAI.ThreeTorus.slowVolume

  43. theorem OAI.ThreeTorus.exists_smooth_reflected_packets line 611

    Source documentation

    Initial smoothing of the SAME supported admissible vector, with exact reflection and arbitrarily small actual full-space L² error.

    theorem exists_smooth_reflected_packets (F : MeasurablePackets)
    {τ : F.Index → F.Index} (hr : F.Reflection τ)
    {δ l u : ℝ} (hδ : 0 ≤ δ) (hd : δ < 1/2) (hdl : δ < l) (hud : u < 1-δ)
    (hsupp : F.Supported l u)
    (V : ℝ → ℝ) (hVp : Periodic V 1)
    (hVs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hVd : ∀ x ∈ Ioo δ (1-δ), 0 < deriv V x)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ G : PassagePackets F.Index, G.m=F.m ∧ G.V=V ∧ G.GoodArc δ ∧
      G.Reflection τ ∧ physicalDist F.vector (finitePacketVector G.m G.A) < ε := by
…

    Mentions: OAI.ThreeTorus.MeasurablePackets, OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.finitePacketVector

  44. lemma OAI.ThreeTorus.physicalDist_zero_eq_norm line 669
  45. lemma OAI.ThreeTorus.MeasurablePackets.flat_norm line 676
  46. lemma OAI.ThreeTorus.MeasurablePackets.smooth_density_distance line 695

    Source documentation

    Smoothing an admissible vector preserves its actual density in L1; the constant is obtained from the SAME two physical packet vectors.

    lemma smooth_density_distance (G : PassagePackets F.Index) (hm : G.m=F.m)
    {φ : UnitAddCircle → UnitAddCircle} (hφ : Measurable φ)
    (hφG : φ=fun u => (G.periodic.lift u:UnitAddCircle)) (hflat : F.spectrum φ=phaseHaar) :
    (∫ z, |(∑ i, G.marginalDensity i z)-1| ∂phaseHaar) ≤
      (physicalDist (finitePacketVector G.m G.A) 0+1)*
        physicalDist F.vector (finitePacketVector G.m G.A) := by
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.finitePacketVector

  47. theorem OAI.ThreeTorus.exists_prepared_pair line 743

    Source documentation

    Source05's full preparation, including both slow insertions. The old admissible vector and the test are compared in their ACTUAL common chart.

    theorem exists_prepared_pair (F : MeasurablePackets)
    {τ : F.Index → F.Index} (hr : F.Reflection τ)
    {δ l u : ℝ} (hδ : 0 ≤ δ) (hd : δ < 1/2) (hdl : δ < l) (hud : u < 1-δ)
    (hsupp : F.Supported l u)
    (V : ℝ → ℝ) (hp : Periodic V 1) (hs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hv : ∀ x ∈ Ioo δ (1-δ), 0 < deriv V x)
    (hflat : F.spectrum (fun z => (hp.lift z:UnitAddCircle))=phaseHaar)
    {h : TripleTorus → ℂ} (hh : Continuous h) (hrh : ∀ x, conj (h x)=h x)
    (hch : ∫ x, h x ∂tripleVolume=0) (hbh : ∀ x, ‖h x‖ ≤ 1)
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    {ε κ ζ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hζ : 0 < ζ) :
    ∃ G H : RealPacketFamily, ∃ α : Equiv.Perm TripleTorus, ∃ frame' : PhysicalFrame,
…

    Mentions: OAI.ThreeTorus.MeasurablePackets, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.H, OAI.ThreeTorus.RealPacketFamily

  48. theorem OAI.ThreeTorus.exists_colored_separation line 816