RootChildMoment.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.integral_sqrt_le_sqrt_integral line 13

Source documentation

Probability-root Jensen for the square root, proved directly from the nonnegative centered square. It is used twice in the multileaf induction.

lemma integral_sqrt_le_sqrt_integral {Z : Type} [MeasurableSpace Z]
    (μ : Measure Z) [IsProbabilityMeasure μ] (f : Z → ℝ)
    (hf : Integrable f μ) (hs : Integrable (fun z => Real.sqrt (f z)) μ)
    (h : ∀ z, 0≤f z) : (∫ z, Real.sqrt (f z) ∂μ)≤Real.sqrt (∫ z, f z ∂μ) := by
…

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootDescendantEnergy_cast line 38
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_sqrt_rootDescendantEnergy_cast line 51
def OAI.DilutedSpinGlass.HeterogeneousMarks.rootChildMeanSum line 73
Source documentation
The actual root child energies, not an independent paired-copy law.
```
noncomputable def rootChildMeanSum : ℝ :=
…
```
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_rootChildSum_le line 78
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_sqrt_rootChildSum_le line 93