OAI/Analysis/FiniteFactor/Sampling/SecondDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingSecondWeight line 11
2. def OAI.FiniteFactor.samplingSecondDensity line 14
3. theorem OAI.FiniteFactor.samplingSecondWeight_measurable line 17
4. theorem OAI.FiniteFactor.samplingSecondWeight_integrable line 22
5. theorem OAI.FiniteFactor.samplingSecondDensity_lintegral line 33
6. theorem OAI.FiniteFactor.samplingSecondDensity_measurable line 39
7. theorem OAI.FiniteFactor.samplingSecondDensity_nonneg line 42
8. theorem OAI.FiniteFactor.sampling_fract_inverse line 46
9. theorem OAI.FiniteFactor.samplingSecondDensity_test line 53

   Source documentation

   Haar substitution identifies the actual second-oriented integral with the weighted endpoint law; no marginal-density hypothesis is assumed.

   theorem samplingSecondDensity_test (h α : ℝ) (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
       (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
       (∫⁻ s, ENNReal.ofReal (samplingSecondDensity h α s)*F s ∂unitIntervalMeasure) =
         ∫⁻ z, ∫⁻ t, ENNReal.ofReal (samplingWeight false h α z t)*F (z+t)
           ∂unitIntervalMeasure ∂unitIntervalMeasure := by
   …

   Mentions: OAI.FiniteFactor.samplingSecondDensity, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingWeight

10. theorem OAI.FiniteFactor.samplingSecondDensity_le_ideal line 98

    Source documentation

    The actual cutoff second marginal is dominated almost everywhere by q_h, completing the missing connection to the quadratic ideal moment.

    theorem samplingSecondDensity_le_ideal (h α : ℝ) (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) :
        ∀ᵐ s ∂unitIntervalMeasure, samplingSecondDensity h α s ≤ samplingIdealSecond h s := by
    …

    Mentions: OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingSecondDensity, OAI.FiniteFactor.samplingIdealSecond