OAI/MeasureTheory/CompactFactors/ConditionalSelection.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EuclideanFiveColor.GoodFiber.exists_lt_on_conull line 28
2. lemma OAI.EuclideanFiveColor.GoodFiber.fraction_lower_bound line 39
3. theorem OAI.EuclideanFiveColor.GoodFiber.simultaneous_good_fiber line 61

   Source documentation

   A single explicit budget gives all small-moment tests and over 90% good approximation indices on the same fiber, together with any conull identities.

   theorem simultaneous_good_fiber (μ : Measure W) [IsProbabilityMeasure μ]
       (f : T → W → ℝ) (e : ι → W → ℝ) (c τ : ℝ) (hc : 0 < c) (hτ : 0 < τ)
       (hf : ∀ t, Integrable (f t) μ) (he : ∀ i, Integrable (e i) μ)
       (hf0 : ∀ᵐ w ∂μ, ∀ t, 0 ≤ f t w) (he0 : ∀ᵐ w ∂μ, ∀ i, 0 ≤ e i w)
       (hbudget : (∑ t, ∫ w, f t w ∂μ)/c +
         10*(∑ i, ∫ w, e i w ∂μ)/((Fintype.card ι : ℝ)*τ) < 1)
       (P : W → Prop) (hP : ∀ᵐ w ∂μ, P w) :
       ∃ w, P w ∧ (∀ t, f t w < c) ∧
         (9/10 : ℝ)*(Fintype.card ι) <
           (Finset.univ.filter (fun i => e i w < τ)).card := by
   …

4. theorem OAI.EuclideanFiveColor.GoodFiber.large_common_bin line 112

   Source documentation

   Pigeonholing happens only after the common good fiber is fixed.

   theorem large_common_bin {L B : ℕ} (s : Finset ι) (b : ι → Fin L)
       (hs : (9/10 : ℝ)*Fintype.card ι < s.card)
       (hLB : (L : ℝ)*B < (9/10 : ℝ)*Fintype.card ι) :
       ∃ J : Finset ι, J ⊆ s ∧ B < J.card ∧ ∀ i ∈ J, ∀ j ∈ J, b i = b j := by
   …

5. lemma OAI.EuclideanFiveColor.Approximation.dist_sq_four_points line 132
6. theorem OAI.EuclideanFiveColor.Approximation.integrated_distance_bound line 149

   Source documentation

   Closeness of approximants costs τ, and each of the two approximation errors costs less than τ in conditional L².

   theorem integrated_distance_bound (μ : Measure X) [IsProbabilityMeasure μ]
       (H A' H₀ A₀ : X → A) (τ : ℝ)
       (hHm : Measurable H) (hH₀m : Measurable H₀)
       (hj : Integrable (fun x => dist (H x) (A' x)^2) μ)
       (h₀ : Integrable (fun x => dist (H₀ x) (A₀ x)^2) μ)
       (hAj : ∫ x, dist (H x) (A' x)^2 ∂μ < τ^2)
       (hA₀ : ∫ x, dist (H₀ x) (A₀ x)^2 ∂μ < τ^2)
       (hbin : ∀ᵐ x ∂μ, dist (A' x) (A₀ x) ≤ τ) :
       Integrable (fun x => dist (H x) (H₀ x)^2) μ ∧
         (∫ x, dist (H x) (H₀ x)^2 ∂μ) < 9*τ^2 := by
   …

7. lemma OAI.EuclideanFiveColor.ConditionalFiber.comp_identity_fiber line 186
8. lemma OAI.EuclideanFiveColor.ConditionalFiber.ae_fiber_of_ae line 192
9. lemma OAI.EuclideanFiveColor.ConditionalFiber.map_identity_fiber line 197
10. lemma OAI.EuclideanFiveColor.ConditionalFiber.ae_in_own_fiber line 205
11. lemma OAI.EuclideanFiveColor.ConditionalFiber.integral_fiber line 218
12. lemma OAI.EuclideanFiveColor.ConditionalFiber.integrable_ae_fiber line 229
13. lemma OAI.EuclideanFiveColor.ConditionalFiber.integrable_fiber_integral line 237
14. theorem OAI.EuclideanFiveColor.FiniteModule.common_fiber_contradiction line 259

    Source documentation

    The actual common-fiber contradiction. The budget is global; all phase upper bounds are required simultaneously on that fiber before a bin is chosen. The phase lists are not assumed measurable.

    theorem common_fiber_contradiction (μ : Measure X) [IsProbabilityMeasure μ]
        (p : X → W) (hp : Measurable p) (m : ℕ) (hm : 0 < m)
        (ρ τ c : ℝ) (hρ : 0 < ρ) (hτ : 0 < τ) (hc : 0 < c)
        (hτδ : 18*τ^2 < (ρ^m/m)^2/20)
        (Hp Hm Ap Am : ι → X → Fin m → ℂ)
        (hHp : ∀ j, Measurable (Hp j)) (hHm : ∀ j, Measurable (Hm j))
        (hIp : ∀ j, Integrable (fun x => dist (Hp j x) (Ap j x)^2) μ)
        (hIm : ∀ j, Integrable (fun x => dist (Hm j x) (Am j x)^2) μ)
        (zp zm : X → ι → Fin m → Circle) (ap am : ι → X → Circle)
        (hap : ∀ j, Measurable (ap j)) (ham : ∀ j, Measurable (am j))
        (henc : ∀ᵐ x ∂μ, ∀ j, PhaseEncoding.encoding (zp x j) = Hp j x ∧
          PhaseEncoding.encoding (zm x j) = Hm j x)
    …

    Mentions: OAI.EuclideanFiveColor.PhaseEncoding.encoding

15. theorem OAI.EuclideanFiveColor.FiniteBins.compact_bins line 377
16. lemma OAI.EuclideanFiveColor.FiniteBins.linear_combination_dist_bound line 401
17. theorem OAI.EuclideanFiveColor.FiniteBins.bounded_coefficient_bins line 417

    Source documentation

    A common finite partition simultaneously controls both coefficient arrays.

    theorem bounded_coefficient_bins (q : ℕ) (B D τ : ℝ) (hD : 0 ≤ D) (hτ : 0 < τ) :
        ∃ L : ℕ, ∃ f : {b : Fin 2 → Fin q → ℂ // ‖b‖ ≤ B} → Fin L,
          ∀ b c, f b = f c → ∀ H : Fin q → V, (∑ i, ‖H i‖) ≤ D →
          ∀ j : Fin 2, dist (∑ i, b.val j i • H i) (∑ i, c.val j i • H i) < τ := by
    …