OAI/Geometry/PinnedDistances/FiberTransport.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_bound line 44
2. lemma OAI.WeakPinned.Hierarchy.Depth.sum_cutLength_univ line 52
3. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_mul line 56
4. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_difference_le line 64
5. lemma OAI.WeakPinned.Hierarchy.Depth.distance_cut_difference line 76
6. lemma OAI.WeakPinned.Hierarchy.Depth.root_cut_difference line 91
7. lemma OAI.WeakPinned.Hierarchy.Depth.cost_cut_formula line 106
8. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_cutLength_param line 114
9. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_cutLength_param line 122
10. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_cutSum_param line 130
11. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_cutDistance_param line 137
12. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_rootDistance_param line 143
13. lemma OAI.WeakPinned.Cuts.tent_lipschitzWith line 151
14. lemma OAI.WeakPinned.Global.arch_cross_defect line 165
15. lemma OAI.WeakPinned.Global.arch_cross_defect_mean line 181
16. lemma OAI.WeakPinned.Global.arch_fiber_cut line 207

    Source documentation

    Actual local cut projection under an arithmetic fiber probability. The atom at y is retained and the source has zero mass.

    lemma arch_fiber_cut (v : NumberField.InfinitePlace K) (p : P → ℝ)
        (hp0 : ∀ z, 0≤p z) (hp : ∑ z, p z=1) (x y : P) (hpx : p x=0) (hpy : p y≠0)
        (t : K) (ht : ∀ z, p z≠0 → (Z₁ x-Z₁ z)*(Z₂ x-Z₂ z)=t)
        (δ : ℝ) (hδ : 0≤δ) (hps : ∀ z, p z≤δ) :
        (∫ ω, |distance (arch Z₁ v ω).allCuts ((arch Z₁ v ω).cutLength (fun C => tent δ (mass p C))) x y-
          rootDistance (arch Z₂ v ω).allCuts ((arch Z₂ v ω).cutLength (fun C => tent δ (mass p C))) y| ∂Grid.fullLaw)≤12 := by
    …

    Mentions: OAI.WeakPinned.Global.arch, OAI.WeakPinned.Grid.fullLaw

17. lemma OAI.WeakPinned.Global.finite_fiber_cut line 259
18. lemma OAI.WeakPinned.Global.integrable_arch_cut_error line 290
19. def OAI.WeakPinned.Global.fiberCutDiscrepancy line 302
20. lemma OAI.WeakPinned.Global.fiber_cut_discrepancy_integrable line 307
21. lemma OAI.WeakPinned.Global.arithmetic_fiber_cut line 323

    Source documentation

    A bounded projection estimate with exact fiber atoms and no restriction on degree, finite places or variation of number fields.

    lemma arithmetic_fiber_cut (w : I → ℝ) (p : I → P → ℝ) (src : I → P) (t : I → K)
        (hw : ∀ i, 0≤w i) (hW : ∑ i, w i=1) (hp0 : ∀ i z, 0≤p i z)
        (hp : ∀ i, ∑ z, p i z=1) (hpx : ∀ i, p i (src i)=0)
        (ht : ∀ i z, p i z≠0 → (Z₁ (src i)-Z₁ z)*(Z₂ (src i)-Z₂ z)=t i)
        (δ : ℝ) (hδ : 0≤δ) (hps : ∀ i z, p i z≤δ) :
        average Z₁ Z₂ h₁ h₂ (fiberCutDiscrepancy w p src δ)≤12 := by
    …

    Mentions: OAI.WeakPinned.Global.average, OAI.WeakPinned.Global.fiberCutDiscrepancy

22. lemma OAI.WeakPinned.Cuts.mass_complement line 374
23. lemma OAI.WeakPinned.Cuts.mass_small line 380
24. lemma OAI.WeakPinned.Cuts.cutError_small line 388
25. lemma OAI.WeakPinned.Cuts.cutError_complement line 394
26. def OAI.WeakPinned.Cuts.charge line 399
27. lemma OAI.WeakPinned.Cuts.charge_nonneg line 402
28. lemma OAI.WeakPinned.Cuts.charge_occurrence line 405
29. lemma OAI.WeakPinned.Cuts.tent_mass_univ line 414
30. lemma OAI.WeakPinned.Cuts.tent_mass_singleton line 419
31. lemma OAI.WeakPinned.Hierarchy.Depth.cutLength_mono line 428
32. lemma OAI.WeakPinned.Cuts.distance_change_charge line 442
33. lemma OAI.WeakPinned.Cuts.root_change_charge line 457
34. lemma OAI.WeakPinned.Cuts.cost_le_charge line 472