OAI/Analysis/BernoulliCone/BoundedCalibration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.DeSilvaJerison.upperFlux line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.upperParameter_signed_pos line 17
3. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_uniform_bound line 25
4. lemma OAI.Bernoulli.DeSilvaJerison.upperSigned_gradient_cap line 43
5. lemma OAI.Bernoulli.DeSilvaJerison.upperSigned_gradient_outer line 51
6. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_eq_calibration line 59
7. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_eventually_eq line 67
8. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_contDiffAt line 80
9. lemma OAI.Bernoulli.DeSilvaJerison.upperParameter_measurable line 84
10. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_measurable line 94
11. lemma OAI.Bernoulli.DeSilvaJerison.upperFlux_intervalIntegrable line 108

    Source documentation

    The height primitive is integrable and has linear growth, using the actual field's uniform bound, independently of seam choices.

    lemma upperFlux_intervalIntegrable (x:Space 7) (a b:ℝ) :
        IntervalIntegrable (fun s:ℝ=>upperFlux (x,s)) MeasureTheory.volume a b := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.upperFlux