FiniteTilt.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.finiteGammaMeasure line 16
Source documentation
The iid Gamma law on a finite set of coordinates.
```
noncomputable def finiteGammaMeasure (shape rate : ℝ) : Measure (ι → ℝ) :=
…
```
def OAI.GammaFPP.finiteGammaScaleLikelihood line 20
Source documentation
Product likelihood for coordinatewise scaling by a.
```
noncomputable def finiteGammaScaleLikelihood (shape rate a : ℝ) (x : ι → ℝ) : ℝ≥0∞ :=
…
```
lemma OAI.GammaFPP.measurable_finiteGammaScaleLikelihood line 23

theorem OAI.GammaFPP.probability_pi_lintegral_prod line 29

Source documentation

Factorization of nonnegative integrals under a finite product of probability measures.

private theorem probability_pi_lintegral_prod (μ : ι → Measure ℝ)
    [∀ i, IsProbabilityMeasure (μ i)] (f : ι → ℝ → ℝ≥0∞)
    (hf : ∀ i, Measurable (f i)) :
    (∫⁻ x, ∏ i, f i (x i) ∂Measure.pi μ) = ∏ i, ∫⁻ y, f i y ∂μ i := by
…

theorem OAI.GammaFPP.indicator_pi_prod line 42
theorem OAI.GammaFPP.finite_gamma_withDensity_scale line 60
Source documentation
Coordinatewise Gamma likelihoods change the rate in the product measure.
```
theorem finite_gamma_withDensity_scale {shape rate a : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (ha : 0 < a) :
    (finiteGammaMeasure (ι := ι) shape rate).withDensity
…
```
Mentions: OAI.GammaFPP.finiteGammaMeasure

theorem OAI.GammaFPP.finite_gamma_map_scale line 89

Source documentation

The pushforward of a finite Gamma law under coordinatewise scaling.

theorem finite_gamma_map_scale {shape rate a : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (ha : 0 < a) :
    (finiteGammaMeasure (ι := ι) shape rate).map (fun x i => a * x i) =
…

Mentions: OAI.GammaFPP.finiteGammaMeasure

theorem OAI.GammaFPP.finite_gamma_map_scale_eq_withDensity line 104
Source documentation
The scaling pushforward equals the measure weighted by the product likelihood.
```
theorem finite_gamma_map_scale_eq_withDensity {shape rate a : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (ha : 0 < a) :
    (finiteGammaMeasure (ι := ι) shape rate).map (fun x i => a * x i) =
…
```
Mentions: OAI.GammaFPP.finiteGammaMeasure

theorem OAI.GammaFPP.finite_gamma_shrink_second_moment_pow line 112

Source documentation

The second moment of the product likelihood factors over the coordinates.

theorem finite_gamma_shrink_second_moment_pow {shape rate delta : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (hlo : -1 < delta) (hhi : delta < 1) :
    (∫⁻ x, (finiteGammaScaleLikelihood (ι := ι) shape rate (1 - delta) x) ^ 2
…

Mentions: OAI.GammaFPP.finiteGammaScaleLikelihood

theorem OAI.GammaFPP.finite_gamma_shrink_second_moment line 129

Source documentation

The second moment is (1 - delta²)^(-shape * N) for -1 < delta < 1, including N = 0.

theorem finite_gamma_shrink_second_moment {shape rate delta : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (hlo : -1 < delta) (hhi : delta < 1) :
    (∫⁻ x, (finiteGammaScaleLikelihood (ι := ι) shape rate (1 - delta) x) ^ 2
…

Mentions: OAI.GammaFPP.finiteGammaScaleLikelihood