OAI/Probability/GammaPassage/FiniteEdgeTilt.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.Tilt.scaleFiniteEdges line 12
2. theorem OAI.GammaFPP.Tilt.scaleFiniteEdges_event_iff line 15
3. theorem OAI.GammaFPP.Tilt.finite_support_event_probability line 26

   Source documentation

   Exact reduction of a supported configuration event to its finite law.

   theorem finite_support_event_probability (h : GammaEnvironment shape rate P τ)
       (S : Finset Edge) (A : Set (Edge → ℝ)) (hA : MeasurableSet A) (hS : DependsOnEdges A S) :
       P {ω | (fun e => τ e ω) ∈ A}=
         (Measure.pi (fun _ : S => gammaMeasure shape rate)) ((extendEdgeWeights S) ⁻¹' A) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment

4. theorem OAI.GammaFPP.Tilt.finite_support_scaled_event_probability line 36
5. theorem OAI.GammaFPP.Tilt.finite_edge_tilt_probability_sq_bound line 54

   Source documentation

   Exact Gamma cost: the shape factor is retained for every positive shape.

   theorem finite_edge_tilt_probability_sq_bound
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (S : Finset Edge) (δ : ℝ) (hlo : -1 < δ) (hhi : δ < 1)
       (A : Set (Edge → ℝ)) (hA : MeasurableSet A) (hS : DependsOnEdges A S) :
       P.real {ω | scaleFiniteEdges S (1-δ) (fun e => τ e ω) ∈ A} ^ 2 ≤
         (1-δ^2)^(-shape * (S.card : ℝ)) * P.real {ω | (fun e => τ e ω) ∈ A} := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.Tilt.scaleFiniteEdges