OAI/Geometry/PinnedDistances/UnboundedContradiction.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Hierarchy.Depth.transformed_half line 14
2. lemma OAI.WeakPinned.Hierarchy.Depth.mass_half line 26
3. lemma OAI.WeakPinned.Global.cellMass_half line 39
4. lemma OAI.WeakPinned.Global.totalMass_half line 42
5. lemma OAI.WeakPinned.Variance.uniform_slice_nonneg line 63
6. lemma OAI.WeakPinned.Variance.edgeCell_le_one line 72
7. lemma OAI.WeakPinned.Variance.balanced_mass_extraction line 86

   Source documentation

   Positive balanced cut length pays all q-overlap except the small-fiber slice and cell variance. This is the exact occurrence extraction inequality.

   lemma balanced_mass_extraction (m : Finset P → ℝ) (hm : ∀ C, 0 ≤ m C)
       (hhalf : ∀ C, 1/2<cellProb Finset.univ C → m C=0)
       (w : I → ℝ) (B : I → Finset P) (src : I → P) (T δ : ℝ)
       (hw : ∀ i, 0≤w i) (hW : (∑ i, w i)≤1) (hδ : 0<δ) (_hδ4 : δ≤1/4)
       (hk : ∀ i, 2/((B i).card:ℝ)≤4*δ) :
       weightedIntegral m (edgeCell w (fun i => prob (B i)) src)≤
         weightedIntegral m (slice w (fun i => prob (B i)) src (4*δ))+
         (1/δ)*weightedIntegral m (varianceCell w B T)+
         (1/δ)*weightedIntegral m (fun C => tent δ (cellProb Finset.univ C)) := by
   …

   Mentions: OAI.WeakPinned.Variance.cellProb, OAI.WeakPinned.B, OAI.WeakPinned.Variance.weightedIntegral, OAI.WeakPinned.Variance.prob, OAI.WeakPinned.Variance.varianceCell

8. lemma OAI.WeakPinned.change_scale_rate line 140
9. lemma OAI.WeakPinned.balanced_extraction_rate line 157
10. theorem OAI.WeakPinned.arithmetic_balanced_length line 205

    Source documentation

    The positive balanced-length estimate of the unbounded branch, on the actual varying-field arithmetic models.

    theorem arithmetic_balanced_length (hθ : 0<θ) (hγ : 0<γ) (hγ1 : γ<1) (hcγ : c<γ)
        (hn : Tendsto (fun j => (Fintype.card (V j):ℝ)) atTop atTop)
        (hη : Tendsto η atTop (𝓝 0)) (hη0 : ∀ j, 0≤η j) (hηb : ∀ j, η j≤θ/2)
        (hG : ∀ j, PreparedGraph (V j) (I j) (G j) θ γ c (η j))
        (t : ∀ j, I j → K j) (ht : ∀ j e y, y ∈ (G j).targets e →
          (Z₁ j ((G j).source e)-Z₁ j y)*(Z₂ j ((G j).source e)-Z₂ j y)=t j e)
        (hWtop : Tendsto (fun j => overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)) atTop atTop) :
        ∃ δ : ℝ, 0<δ ∧ δ≤1/8 ∧ ∀ᶠ j in atTop,
          (δ/4)*overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j) ≤
            weightedIntegral (totalMass (Z₁ j) (Z₂ j) (h₁ j) (h₂ j))
              (fun C => tent δ (cellProb Finset.univ C)) := by
    …

    Mentions: OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.overlapScale

11. lemma OAI.WeakPinned.Cuts.tent_length_occurrence line 307
12. lemma OAI.WeakPinned.Global.average_swap line 327
13. lemma OAI.WeakPinned.Global.integrable_weighted_left line 335
14. lemma OAI.WeakPinned.Global.integrable_weighted_right line 344
15. lemma OAI.WeakPinned.Global.average_weighted_left line 351
16. lemma OAI.WeakPinned.Global.average_weighted_right line 357
17. def OAI.WeakPinned.Global.localTotalIntegral line 363
18. lemma OAI.WeakPinned.Global.integrable_total_integral line 368
19. lemma OAI.WeakPinned.Global.average_total_integral line 372
20. lemma OAI.WeakPinned.Core.Fibers.two_length_upper line 386
21. lemma OAI.WeakPinned.Global.arithmetic_length_upper line 412
22. lemma OAI.WeakPinned.prob_bound_of_size line 464
23. lemma OAI.WeakPinned.PreparedGraph.omitted_bound line 474
24. lemma OAI.WeakPinned.omitted_rate line 497
25. lemma OAI.WeakPinned.sampling_atoms_eventually line 508
26. lemma OAI.WeakPinned.length_rate_contradiction line 533
27. theorem OAI.WeakPinned.arithmetic_no_unbounded line 563

    Source documentation

    The entire unbounded regime is impossible for the actual prepared arithmetic models, allowing arbitrary and varying number fields.

    theorem arithmetic_no_unbounded (hθ : 0<θ) (hγ : 0<γ) (hγ1 : γ<1) (hc : 0<c) (hcγ : c<γ)
        (hn : Tendsto (fun j => (Fintype.card (V j):ℝ)) atTop atTop)
        (hη : Tendsto η atTop (𝓝 0)) (hη0 : ∀ j, 0≤η j) (hηb : ∀ j, η j≤θ/2)
        (hG : ∀ j, PreparedGraph (V j) (I j) (G j) θ γ c (η j))
        (t : ∀ j, I j → K j) (ht : ∀ j e y, y∈(G j).targets e →
          (Z₁ j ((G j).source e)-Z₁ j y)*(Z₂ j ((G j).source e)-Z₂ j y)=t j e)
        (hWtop : Tendsto (fun j => overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)) atTop atTop) : False := by
    …

    Mentions: OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.overlapScale