OAI/Geometry/PinnedDistances/TreeContradiction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Cuts.cost_mixture line 47
2. lemma OAI.WeakPinned.Cuts.mass_upper line 70
3. lemma OAI.WeakPinned.Cuts.cost_bound line 74
4. lemma OAI.WeakPinned.Cuts.projection_replacement line 83
5. lemma OAI.WeakPinned.Cuts.family_charge_occurrence line 105
6. lemma OAI.WeakPinned.Cuts.length_upper line 126

   Source documentation

   One coordinate of the finite tree contradiction, before arithmetic averaging. The incoming laws are arbitrary probabilities representing the actual conditional source law, not an independence hypothesis.

   lemma length_upper (d d' : Depth P) (δ : ℝ) (hδ : 0≤δ)
       (a t : P → ℝ) (ρ : P → P → ℝ) (w : I → ℝ) (p : I → P → ℝ) (src : I → P)
       (ha0 : ∀ x, 0≤a x) (ht0 : ∀ y, 0≤t y) (hρ0 : ∀ y x, 0≤ρ y x) (hw : ∀ i, 0≤w i)
       (ha : ∑ x, a x=1) (ht : ∑ y, t y=1) (hρ : ∀ y, ∑ x, ρ y x=1) (hW : ∑ i, w i=1)
       (hp : ∀ i, ∑ y, p i y=1) (hp0 : ∀ i y, 0≤p i y)
       (has : ∀ x, a x≤δ) (hps : ∀ i x, p i x≤δ)
       (htm : t=fun y => ∑ i, w i*p i y)
       (hedge : ∀ F : P → P → ℝ, (∑ y, t y*∑ x, ρ y x*F x y)=∑ i, w i*∑ y, p i y*F (src i) y) :
       δ^3*(∑ C ∈ d.allCuts, d.cutLength (fun B => tent δ (mass a B)) C)≤
         2*Global.fiberCutDiscrepancy w p src δ d d'+
         4*(∑ i, w i*charge d δ (p i) a)+2*(∑ i, w i*charge d' δ (p i) a)+
         2*(∑ y, t y*cost d.allCuts (d.cutLength (fun B => tent δ (mass a B))) (ρ y) a) := by
   …

   Mentions: OAI.WeakPinned.F, OAI.WeakPinned.B, OAI.WeakPinned.Cuts.tent, OAI.WeakPinned.Cuts.mass, OAI.WeakPinned.Global.fiberCutDiscrepancy, OAI.WeakPinned.Cuts.charge, OAI.WeakPinned.Cuts.cost

7. lemma OAI.WeakPinned.Core.Fibers.prob_nn line 170
8. def OAI.WeakPinned.Core.Fibers.conditionalSource line 174
9. lemma OAI.WeakPinned.Core.Fibers.conditionalSource_nonneg line 178
10. lemma OAI.WeakPinned.Core.Fibers.conditionalSource_sum line 183
11. lemma OAI.WeakPinned.Core.Fibers.incomingWeight_nonneg line 190
12. lemma OAI.WeakPinned.Core.Fibers.sampling_conditional line 193
13. lemma OAI.WeakPinned.Core.Fibers.incoming_eval line 202
14. lemma OAI.WeakPinned.Core.Fibers.incoming_repr line 218
15. def OAI.WeakPinned.Core.Fibers.omittedMass line 222
16. lemma OAI.WeakPinned.Core.Fibers.omittedMass_nonneg line 225
17. lemma OAI.WeakPinned.Core.Fibers.retained_cost line 233
18. lemma OAI.WeakPinned.Core.Fibers.graph_length_upper line 262