OAI/Analysis/PlaneSpectrum/SmallArcs.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Fiberwise (possibly nonmeasurable) enumerations cause no measurability gap: actual conditional samples lie in them by the measurable positive-atom event.

  1. def OAI.EuclideanFiveColor.SmallArc.phaseSum line 33
  2. lemma OAI.EuclideanFiveColor.SmallArc.pow_sub_one_bound line 35
  3. lemma OAI.EuclideanFiveColor.SmallArc.phaseSum_sub_bound line 49
  4. lemma OAI.EuclideanFiveColor.SmallArc.phaseSum_lower line 64
  5. lemma OAI.EuclideanFiveColor.SmallArc.phase_energy line 79
  6. lemma OAI.EuclideanFiveColor.SmallArc.pow_mul_conj_pow line 92
  7. lemma OAI.EuclideanFiveColor.SmallArc.integrable_pair line 102
  8. lemma OAI.EuclideanFiveColor.SmallArc.pair_moment_bound line 107
  9. lemma OAI.EuclideanFiveColor.SmallArc.phase_energy_integral_bound line 134
  10. lemma OAI.EuclideanFiveColor.SmallArc.integrable_energy line 166
  11. theorem OAI.EuclideanFiveColor.SmallArc.small_arc_bound line 178

    Source documentation

    A quantitative finite-moment bound for the small arc about 1.

    theorem small_arc_bound {N : ℕ} (hN : 0 < N) {c : ℝ} (hc : 0 ≤ c)
    (hm : ∀ n, 0 < n → n < N → ‖∫ x, z x ^ n ∂μ‖ ≤ c) :
    μ.real {x | ‖z x-1‖ ≤ 1 / (2 * (N : ℝ))} ≤ 4 / N + 4*c := by
…
  12. theorem OAI.EuclideanFiveColor.SmallArc.exists_small_arc_constants line 206

    Source documentation

    The source's qualitative choice, with explicit constants.

    theorem exists_small_arc_constants (m : ℕ) (hm : 0 < m) :
    ∃ (ρ c : ℝ) (N : ℕ), 0 < ρ ∧ 0 < c ∧ 0 < N ∧
      ∀ (ω : Measure Circle) [IsProbabilityMeasure ω],
      (∀ n, 0 < n → n ≤ N → ‖∫ w, (w : ℂ)^n ∂ω‖ < c) →
      ω.real {w | ‖(w : ℂ)-1‖ ≤ 4*ρ} < 1/(4*(m : ℝ)^2) := by
…
  13. lemma OAI.EuclideanFiveColor.SampledAtoms.measurable_atom_mass line 242
  14. lemma OAI.EuclideanFiveColor.SampledAtoms.ae_sampled_positive_atom line 258
  15. lemma OAI.EuclideanFiveColor.SampledAtoms.uniform_list_positive_atoms line 270
  16. lemma OAI.EuclideanFiveColor.SampledAtoms.in_list_of_positive_atom line 292
  17. lemma OAI.EuclideanFiveColor.SampledAtoms.ae_sampled_list line 303