OAI/Analysis/PlaneSpectrum/ConditionalSpectrum.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PlaneFiveColor.Spectral.dualPolishSpace line 38
2. def OAI.PlaneFiveColor.Spectral.eval line 47

   Source documentation

   Evaluation at the exact algebraic argument.

   def eval (a : E) : D →* Circle where
   …

   Mentions: OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.D

3. lemma OAI.PlaneFiveColor.Spectral.continuous_eval line 52
4. lemma OAI.PlaneFiveColor.Spectral.measurable_eval line 56
5. lemma OAI.PlaneFiveColor.Spectral.measurable_eval_coe line 57
6. lemma OAI.PlaneFiveColor.Spectral.eval_zero line 61
7. lemma OAI.PlaneFiveColor.Spectral.eval_add line 62
8. lemma OAI.PlaneFiveColor.Spectral.eval_neg line 64
9. lemma OAI.PlaneFiveColor.Spectral.eval_sub line 66
10. lemma OAI.PlaneFiveColor.Spectral.eval_nat_mul line 68
11. lemma OAI.PlaneFiveColor.Spectral.eval_scalar line 73
12. lemma OAI.PlaneFiveColor.Spectral.eval_smul_one line 74
13. lemma OAI.PlaneFiveColor.Spectral.lineFourier_eq line 77
14. lemma OAI.PlaneFiveColor.Spectral.predecessor_moment_sq line 85

    Source documentation

    The actual conditional moment on a predecessor fiber is the Fourier coefficient of the actual relative difference law, not an extra hypothesis.

    lemma predecessor_moment_sq (μ : Measure X) [IsProbabilityMeasure μ]
        (p : X → W) (b : X → D) (hp : Measurable p) (hb : Measurable b) (a : E) :
        (∫ w, ‖∫ x, (eval a (b x) : ℂ) ∂condDistrib id p μ w‖^2 ∂μ.map p) =
          (∫ d, (eval a d : ℂ) ∂DifferenceFourier.differenceLaw (μ.map p)
            (condDistrib b p μ)).re := by
    …

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.eval

15. lemma OAI.PlaneFiveColor.Spectral.integrable_predecessor_moment_sq line 99
16. theorem OAI.PlaneFiveColor.Spectral.real_algebraic_sum_two_rotations line 116
17. theorem OAI.EuclideanFiveColor.PhaseEncoding.kernelEncoding_covariance line 160

    Source documentation

    Covariance of the actual Newton-symmetric conditional encoding.

    theorem kernelEncoding_covariance (ν : Measure Y) (β : Kernel Y G)
        (R : Y → Y) (T : G → G) (hT : Measurable T)
        (χ : G → ℂ) (hχ : Measurable χ) (m : ℕ)
        (hβ : ∀ᵐ y ∂ν, β (R y) = (β y).map T) :
        ∀ᵐ y ∂ν, kernelEncoding β χ m (R y) = kernelEncoding β (χ ∘ T) m y := by
    …

    Mentions: OAI.EuclideanFiveColor.PhaseEncoding.kernelEncoding

18. abbrev OAI.PlaneFiveColor.Spectral.MomentTest line 181
19. def OAI.PlaneFiveColor.Spectral.momentArgument line 183
20. lemma OAI.PlaneFiveColor.Spectral.momentArgument_ne_zero line 186
21. lemma OAI.PlaneFiveColor.Spectral.momentTest_nonempty line 195
22. theorem OAI.PlaneFiveColor.Spectral.exists_simultaneous_moment_parameter line 204

    Source documentation

    All integer multiples of all distinct pair differences are tested before any coefficient bin is selected.

    theorem exists_simultaneous_moment_parameter (ν : Measure D) [IsProbabilityMeasure ν]
        (hν : IsWild ν) (hn : ∀ a : E, 0 ≤ (∫ d, (eval a d : ℂ) ∂ν).re)
        (M N : ℕ) (hM : 2 ≤ M) (hN : 0 < N) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) :
        ∃ t : F, t ≠ 0 ∧ |(t : ℝ)| < 1/(M : ℝ) ∧
          ∀ z : MomentTest M N, (∫ d, (eval (momentArgument z * ofF t) d : ℂ) ∂ν).re < ε := by
    …

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.IsWild, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.eval, OAI.PlaneFiveColor.Spectral.F, OAI.PlaneFiveColor.Spectral.MomentTest, OAI.PlaneFiveColor.Spectral.momentArgument, OAI.PlaneFiveColor.Spectral.ofF

23. lemma OAI.PlaneFiveColor.Spectral.eval_dist line 218
24. theorem OAI.PlaneFiveColor.Spectral.pair_collision_upper line 228

    Source documentation

    The finite Fejér implication is applied to the actual phase law on an individual conditional fiber.

    theorem pair_collision_upper {X : Type*} [MeasurableSpace X]
        (μ : Measure X) [IsProbabilityMeasure μ] (b : X → D) (hb : Measurable b)
        (a₁ a₂ : E) (m N : ℕ) (ρ c : ℝ)
        (harc : ∀ (ω : Measure Circle) [IsProbabilityMeasure ω],
          (∀ n, 0 < n → n ≤ N → ‖∫ w, (w : ℂ)^n ∂ω‖ < c) →
          ω.real {w | ‖(w : ℂ)-1‖ ≤ 4*ρ} < 1/(4*(m : ℝ)^2))
        (hMom : ∀ n, 0 < n → n ≤ N →
          ‖∫ x, (eval ((n : E)*(a₁-a₂)) (b x) : ℂ) ∂μ‖ < c) :
        μ.real {x | dist (eval a₁ (b x) : ℂ) (eval a₂ (b x) : ℂ) ≤ 4*ρ}
          < 1/(4*(m : ℝ)^2) := by
    …

    Mentions: OAI.PlaneFiveColor.Spectral.D, OAI.PlaneFiveColor.Spectral.E, OAI.PlaneFiveColor.Spectral.eval

25. def OAI.PlaneFiveColor.Spectral.FiniteEncodingApproximationAt line 267
26. def OAI.PlaneFiveColor.Spectral.FiniteEncodingApproximation line 282
27. lemma OAI.PlaneFiveColor.Spectral.two_array_norm_bound line 286
28. lemma OAI.PlaneFiveColor.Spectral.simultaneous_test_budget line 292
29. theorem OAI.PlaneFiveColor.Spectral.finite_uniform_precision_contradiction line 310
30. theorem OAI.PlaneFiveColor.Spectral.finite_uniform_successor_contradiction line 479