import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Probability.Moments.SubGaussian
import Mathlib.Probability.Moments.MGFAnalytic
import Mathlib.Analysis.Convex.Integral

/-! # Standalone extraction for `ProbabilityTheory.Kernel.HasSubexponentialMGF.id_map_iff`
Definitions are copied verbatim; theorem proofs are replaced by `sorry`.
Auto-generated by ChallengeGen. -/

set_option quotPrecheck false

-- Namespace stubs (so later `open`s resolve).
namespace Finset
end Finset
namespace MeasureTheory
end MeasureTheory
namespace ENNReal
end ENNReal
namespace ProbabilityTheory
end ProbabilityTheory
namespace ProbabilityTheory.Kernel.HasSubexponentialMGF
end ProbabilityTheory.Kernel.HasSubexponentialMGF

-- ═══ ForMathlib.MeasureTheory.Order.Lattice ═══
section
open Finset
variable {α δ : Type*} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α} [MeasurableInf₂ α]
attribute [to_dual existing] MeasurableInf₂
end

-- ═══ ForMathlib.Probability.Moments.SubExponential ═══
section
open MeasureTheory Real Finset
open scoped ENNReal NNReal Topology
namespace ProbabilityTheory
section Kernel
variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ}

/-- A random variable `X` has a sub-exponential moment-generating function with parameters
`(V, b)` with respect to a kernel `κ` and a measure `ν` if for every `t` with `b * |t| ≤ 1`,
`exp (t * X)` is integrable with respect to `κ ∘ₘ ν` and, for `ν`-almost all `ω'`,
the moment-generating function of `X` with respect to `κ ω'` is bounded by `exp (V * t ^ 2 / 2)`.
For `b = 0` this is `Kernel.HasSubgaussianMGF X V κ ν`. -/
structure Kernel.HasSubexponentialMGF (X : Ω → ℝ) (V b : ℝ)
    (κ : Kernel Ω' Ω) (ν : Measure Ω' := sorry) : Prop where
  integrable_exp_mul : ∀ t, b * |t| ≤ 1 → Integrable (fun ω ↦ exp (t * X ω)) (κ ∘ₘ ν)
  mgf_le : ∀ᵐ ω' ∂ν, ∀ t, b * |t| ≤ 1 → mgf X (κ ω') t ≤ exp (V * t ^ 2 / 2)

namespace Kernel.HasSubexponentialMGF

lemma id_map_iff (hX : Measurable X) :
    HasSubexponentialMGF id V b (κ.map X) ν ↔ HasSubexponentialMGF X V b κ ν := sorry

end Kernel.HasSubexponentialMGF
end Kernel
variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : Ω → ℝ} {V b : ℝ}
end ProbabilityTheory
end