ML.Core · Causalean Library

Hypothesis 3 core · 0 supporting The standalone ML spine carries two views of a learning method, connected by Causalean.ML.Core.Bridge: * the parametric view (Predictor): a parameter type Θ together with an admissible set and a prediction map Θ → X → Y. ★ Predictor★ HypothesisClass★ FeatureMap

Hypothesis classes and parametrized predictors

The standalone ML spine carries two views of a learning method, connected by Causalean.ML.Core.Bridge:

* the parametric view (Predictor): a parameter type Θ together with an admissible set and a prediction map Θ → X → Y. Optimization, convexity and regularization live here. * the extensional view (HypothesisClass): a set of measurable functions X → Y. Population-risk targets and best-in-class statements live here.

FeatureMap packages a feature transform X → (K → ℝ) so that linear-in-features regression (and hence series/sieve regression) is a single object.

structure Predictor reviewed

Causalean.ML

A parametrized family of predictors bundles an admissible set of parameter values together with a map sending each parameter to a prediction function from the covariates to the outcome.

Definition (Lean source)

parameters

Θ X Y :

Type*

fields

The admissible parameter set (e.g. a norm ball, or all of `Θ`).

paramSet :

Set Θ

The prediction map: a parameter yields a function `X → Y`.

predict :

Θ → X → Y

Causalean.ML.Predictor · Causalean/ML/Core/Hypothesis.lean:31

structure HypothesisClass reviewed

Causalean.ML

A hypothesis class packaged extensionally as a set of admissible prediction functions from the covariates to the outcome, subject to the requirement that every function admitted to the class is measurable.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

fields

The set of admissible prediction functions.

carrier :

Set (X → Y)

Every admissible function is measurable.

measurable :

∀ ⦃h : X → Y⦄

if

h ∈ carrier

then

Measurable h

Causalean.ML.HypothesisClass · Causalean/ML/Core/Hypothesis.lean:40

structure FeatureMap reviewed

Causalean.ML

A finite feature map bundles a transform sending each input to its vector of K feature values. Linear-in-features predictors use x ↦ ⟪β, φ x⟫; the identity feature map recovers ordinary linear regression, and other choices of the transform recover polynomial, spline, or Fourier (sieve) regression.

Definition (Lean source)

parameters

X :

Type*

K :

Type*

Fintype K

fields

The feature transform sending an input to its vector of feature values.

φ :

X → (K → ℝ)

Causalean.ML.FeatureMap · Causalean/ML/Core/Hypothesis.lean:49

Risk 7 core · 0 supporting Risk criteria for the ML spine, in both the parametric and extensional views. ★ Loss★ empiricalRisk★ populationRisk

Empirical and population risk

Risk criteria for the ML spine, in both the parametric and extensional views. Loss is a pointwise prediction-label loss, empiricalRisk and empiricalRiskP are nonempty finite-sample averages, populationRisk and populationRiskP are Bochner-integral population criteria, and iidEmpiricalRisk expresses empirical risk through Stat.IIDSample.sampleMean. The separate predicate HasFinitePopulationRisk records when the population integral has the usual finite expected-loss interpretation.

abbrev Loss reviewed

Causalean.ML

A pointwise loss assigns a real penalty to predicted and observed labels by comparing one label-space value with another.

Definition (Lean source)

parameters

Y :

Type*

def

Loss Y :

Type u_1

given by

Y → Y → ℝ

Causalean.ML.Loss · Causalean/ML/Core/Risk.lean:29

def empiricalRisk reviewed

Causalean.ML

Empirical risk is average loss over a nonempty finite sample. It evaluates a prediction rule with a pointwise loss on sampled input--label pairs indexed by a finite nonempty set, with input and label spaces.

Definition (Lean source)

parameters

ι X Y :

Type*

Fintype ι

Nonempty ι

loss :

Loss Y

S :

ι → X × Y

h :

X → Y

def

empiricalRisk loss S h :

ℝ

given by

(Fintype.card ι : ℝ)⁻¹ * ∑ i, loss (h (S i).1) (S i).2

Causalean.ML.empiricalRisk · Causalean/ML/Core/Risk.lean:33 · uses Loss

def empiricalRiskP reviewed

Causalean.ML

Parametric empirical risk assigns a parameter value the sample-average loss of its prediction rule. The rule comes from a parametrized predictor on parameter, input, and label spaces, using the chosen loss and sample over a nonempty finite index set.

Definition (Lean source)

parameters

ι Θ X Y :

Type*

Fintype ι

Nonempty ι

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

θ :

Θ

def

empiricalRiskP M loss S θ :

ℝ

given by

empiricalRisk loss S (M.predict θ)

Causalean.ML.empiricalRiskP · Causalean/ML/Core/Risk.lean:41 · uses Loss , Predictor

def populationRisk reviewed

Causalean.ML

Population risk is the expected pointwise prediction loss of a prediction rule under a joint input--label law, using a chosen loss function on measurable input and label spaces.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

loss :

Loss Y

P :

Measure (X × Y)

h :

X → Y

def

populationRisk loss P h :

ℝ

given by

∫ z, loss (h z.1) z.2 ∂P

Causalean.ML.populationRisk · Causalean/ML/Core/Risk.lean:49 · uses Loss

def populationRiskP reviewed

Causalean.ML

Parametric population risk assigns a parameter value the expected loss of its prediction rule. The rule comes from a parametrized predictor on parameter, measurable input, and measurable label spaces, and is evaluated with the chosen loss under the joint input--label law.

Definition (Lean source)

parameters

Θ X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

P :

Measure (X × Y)

θ :

Θ

def

populationRiskP M loss P θ :

ℝ

given by

populationRisk loss P (M.predict θ)

Causalean.ML.populationRiskP · Causalean/ML/Core/Risk.lean:58 · uses Loss , Predictor

def iidEmpiricalRisk reviewed

Causalean.ML

The i.i.d. empirical risk is random average loss over the requested prefix from an i.i.d. input--label sample. It evaluates a prediction rule with the chosen loss at the sample size, under experiment and population laws on the measurable sample, input, and label spaces.

Definition (Lean source)

parameters

Ω X Y :

Type*

MeasurableSpace Ω

MeasurableSpace (X × Y)

Measure Ω

Measure (X × Y)

S :

IIDSample Ω (X × Y) μ P

loss :

Loss Y

h :

X → Y

n :

ℕ

def

iidEmpiricalRisk S loss h n :

Ω → ℝ

given by

S.sampleMean (fun z => loss (h z.1) z.2) n

Causalean.ML.iidEmpiricalRisk · Causalean/ML/Core/Risk.lean:67 · uses Loss , IIDSample

def HasFinitePopulationRisk reviewed

Causalean.ML

Finite population risk requires integrability of prediction loss under the joint law. It applies to a prediction rule and pointwise loss under that joint law on measurable input and label spaces.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

loss :

Loss Y

P :

Measure (X × Y)

h :

X → Y

def

HasFinitePopulationRisk loss P h :

Prop

given by

Integrable (fun z => loss (h z.1) z.2) P

Causalean.ML.HasFinitePopulationRisk · Causalean/ML/Core/Risk.lean:79 · uses Loss

ERM 5 core · 0 supporting Minimizer predicates for the ML spine, stated candidate-wise via Mathlib's IsMinOn (or a comparison + ε form), never via sInf/argmin — this avoids pathological real-infimum defaults on empty or unbounded sets, matching t ★ IsERMP★ RegularizedERM★ IsERM

Empirical-risk-minimizer predicates

Minimizer predicates for the ML spine, stated candidate-wise via Mathlib's IsMinOn (or a comparison + ε form), never via sInf/argmin — this avoids pathological real-infimum defaults on empty or unbounded sets, matching the existing Estimation.OrthogonalLearning.PluginERM idiom.

The file provides exact, approximate, and regularized parametric ERM predicates (IsERMP, IsApproxERMP, RegularizedERM), plus extensional empirical and population minimizer predicates (IsERM, IsPopulationRiskMinimizer) over a HypothesisClass. The parametric and extensional views are connected in Causalean.ML.Core.Bridge.

structure IsERMP reviewed

Causalean.ML

θhat exactly minimizes a parametric objective over the admissible set.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

Θset :

Set Θ

θhat :

Θ

assumes

mem :

θhat ∈ Θset

The minimizer is admissible.

isMin :

IsMinOn objective Θset θhat

It attains the minimum of the objective over Θset.

Causalean.ML.IsERMP · Causalean/ML/Core/ERM.lean:31

structure IsApproxERMP reviewed

Causalean.ML

θhat minimizes a parametric objective up to slack ε ≥ 0.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

Θset :

Set Θ

θhat :

Θ

ε :

ℝ

assumes

ε_nonneg :

0 ≤ ε

The slack is nonnegative.

mem :

θhat ∈ Θset

The candidate is admissible.

approx_min :

∀ θ ∈ Θset, objective θhat ≤ objective θ + ε

Its objective is within ε of every competitor's.

Causalean.ML.IsApproxERMP · Causalean/ML/Core/ERM.lean:38

structure RegularizedERM reviewed

Causalean.ML

θhat minimizes a penalized objective objective θ + lam · penalty θ with a nonnegative regularization weight lam.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

penalty :

Θ → ℝ

lam :

ℝ

Θset :

Set Θ

θhat :

Θ

assumes

lam_nonneg :

0 ≤ lam

The regularization weight is nonnegative.

mem :

θhat ∈ Θset

The minimizer is admissible.

isMin :

IsMinOn (fun θ => objective θ + lam * penalty θ) Θset θhat

It minimizes the penalized objective over Θset.

Causalean.ML.RegularizedERM · Causalean/ML/Core/ERM.lean:48

structure IsERM reviewed

Causalean.ML

An empirical-risk minimizer is an admissible prediction rule whose finite-sample risk criterion is no larger than that of any other admissible rule. The criterion is the inverse-cardinality-scaled loss sum over a nonempty finite sample.

Definition (Lean source)

parameters

ι X Y :

Type*

Fintype ι

Nonempty ι

MeasurableSpace X

MeasurableSpace Y

H :

HypothesisClass X Y

loss :

Loss Y

S :

ι → X × Y

hhat :

X → Y

assumes

mem :

hhat ∈ H.carrier

The minimizer belongs to the class.

isMin :

IsMinOn (fun h => empiricalRisk loss S h) H.carrier hhat

It minimizes empirical risk over the class.

Causalean.ML.IsERM · Causalean/ML/Core/ERM.lean:59 · uses HypothesisClass , Loss

structure IsPopulationRiskMinimizer reviewed

Causalean.ML

A population-risk minimizer bundles the claim that a prediction rule belongs to the hypothesis class, that it has finite expected loss under the population measure, that every other rule admissible in the class also has finite expected loss, and that its population risk is no larger than that of any other rule in the class.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

H :

HypothesisClass X Y

loss :

Loss Y

P :

Measure (X × Y)

hstar :

X → Y

assumes

mem :

hstar ∈ H.carrier

The minimizer belongs to the class.

finite_self :

HasFinitePopulationRisk loss P hstar

The minimizer has finite expected loss.

finite_competitor :

∀ h ∈ H.carrier, HasFinitePopulationRisk loss P h

Every admissible competitor has finite expected loss.

isMin :

IsMinOn (fun h => populationRisk loss P h) H.carrier hstar

It minimizes population risk over the class.

Causalean.ML.IsPopulationRiskMinimizer · Causalean/ML/Core/ERM.lean:71 · uses HypothesisClass , Loss

Losses 5 core · 5 supporting This file collects the elementary pointwise loss functions used throughout Causalean.ML: squared loss for regression, Boolean-to-real encoding, softplus, and score-space logistic loss for binary classification. ★ squaredLoss★ logisticScoreLoss★ squaredLoss_nonneg

Loss functions for the standalone ML module

This file collects the elementary pointwise loss functions used throughout Causalean.ML: squared loss for regression, Boolean-to-real encoding, softplus, and score-space logistic loss for binary classification. Logistic models use Mathlib's canonical Real.sigmoid. Everything here is causal-free real analysis; no probability or causal layer is imported.

def squaredLoss reviewed

Causalean.ML

Squared loss measures a real-valued prediction against the observed outcome by squaring their difference.

Definition (Lean source)

parameters

ŷ y :

ℝ

def

squaredLoss ŷ y :

ℝ

given by

(y - ŷ) ^ 2

Causalean.ML.squaredLoss · Causalean/ML/Core/Losses.lean:24

def bool01 reviewed

Causalean.ML

The zero--one real encoding makes a Boolean label available to real-valued loss formulas by mapping true to one and false to zero.

Definition (Lean source)

parameters

b :

Bool

def

bool01 b :

ℝ

given by

if b then 1 else 0

Causalean.ML.bool01 · Causalean/ML/Core/Losses.lean:30

def softplus reviewed

Causalean.ML

Softplus turns an unrestricted real score into the log of one plus its exponential, a smooth positive quantity used in logistic loss.

Definition (Lean source)

parameters

t :

ℝ

def

softplus t :

ℝ

given by

log (1 + exp t)

Causalean.ML.softplus · Causalean/ML/Core/Losses.lean:36

def logisticScoreLoss reviewed

Causalean.ML

The score-space logistic loss evaluates a binary outcome at an unrestricted prediction score as softplus minus the zero--one label times the score.

Definition (Lean source)

parameters

y :

Bool

t :

ℝ

def

logisticScoreLoss y t :

ℝ

given by

softplus t - bool01 y * t

Causalean.ML.logisticScoreLoss · Causalean/ML/Core/Losses.lean:42

lemma squaredLoss_nonneg reviewed

Causalean.ML

Squared prediction error cannot be negative, regardless of the predicted and observed values.

Formal statement

hypotheses

ŷ y :

ℝ

conclusion

0 ≤ squaredLoss ŷ y

Proof (Lean source)

lemma squaredLoss_nonneg (ŷ y : ℝ) : 0 ≤ squaredLoss ŷ y := sq_nonneg _

Causalean.ML.squaredLoss_nonneg · Causalean/ML/Core/Losses.lean:64 · uses squaredLoss

5 supporting declarations (lemmas, instances)

bool01_true lemma — A true Boolean label is encoded as the real number one.

conclusion

bool01 true = 1

Proof (Lean source)

@[simp] lemma bool01_true : bool01 true = 1 := rfl

Causalean.ML.bool01_true · Causalean/ML/Core/Losses.lean:50
bool01_false lemma — A false Boolean label is encoded as zero.

conclusion

bool01 false = 0

Proof (Lean source)

@[simp] lemma bool01_false : bool01 false = 0 := rfl

Causalean.ML.bool01_false · Causalean/ML/Core/Losses.lean:53
bool01_nonneg lemma — The zero-one encoding of a Boolean label is always nonnegative.

hypotheses

b :

Bool

conclusion

0 ≤ bool01 b

Proof (Lean source)

lemma bool01_nonneg (b : Bool) : 0 ≤ bool01 b := by cases b <;> simp [bool01]

Causalean.ML.bool01_nonneg · Causalean/ML/Core/Losses.lean:56
bool01_le_one lemma — The zero-one encoding of a Boolean label is always at most one.

hypotheses

b :

Bool

conclusion

bool01 b ≤ 1

Proof (Lean source)

lemma bool01_le_one (b : Bool) : bool01 b ≤ 1 := by cases b <;> simp [bool01]

Causalean.ML.bool01_le_one · Causalean/ML/Core/Losses.lean:60
softplus_pos lemma — Softplus is strictly positive at every score.

hypotheses

t :

ℝ

conclusion

0 < softplus t

Proof (Lean source)

lemma softplus_pos (t : ℝ) : 0 < softplus t := by have hpos : (0 : ℝ) < exp t := Real.exp_pos _ have h1 : (1 : ℝ) < 1 + exp t := by linarith exact Real.log_pos h1

Causalean.ML.softplus_pos · Causalean/ML/Core/Losses.lean:68

Bridge 2 core · 1 supporting The image of a Predictor under its prediction map is a HypothesisClass, and a *parametric* minimizer pushes forward to an *extensional* minimizer over that image class. ★ populationTarget_pushforward

Bridge between the parametric and extensional views

The image of a Predictor under its prediction map is a HypothesisClass, and a parametric minimizer pushes forward to an extensional minimizer over that image class. These two lemmas are the only glue between the two views of a method: properties stated in parameter space (convexity, regularization, optimization) transfer to the function-class statements (best-in-class, population target).

def imageClass reviewed

Causalean.ML

The realized hypothesis class turns a parametrized predictor into exactly its admissible prediction rules. Measurability of every admissible rule supplies the class-wide measurability guarantee needed for population-risk analysis.

Definition (Lean source)

parameters

Θ X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

M :

Predictor Θ X Y

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

def

imageClass M hmeas :

HypothesisClass X Y

given by

clause 1

carrier := (fun θ => M.predict θ) '' M.paramSet

clause 2

measurable := by rintro h ⟨θ, hθ, rfl⟩ exact hmeas θ hθ

Causalean.ML.imageClass · Causalean/ML/Core/Bridge.lean:26 · uses HypothesisClass , Predictor

theorem populationTarget_pushforward reviewed

Causalean.ML

Population-target pushforward. For a predictor M with loss loss and population law P, suppose every admissible parameter's prediction function is measurable, the parameter θhat is itself admissible, every admissible parameter attains finite population risk, and θhat minimizes the population risk over the admissible parameter set. Then the predictor M.predict θhat is a population-risk minimizer over the hypothesis class realized by M's image: a parametric population-risk minimizer pushes forward to an extensional minimizer over the realized function class.

Formal statement

hypotheses

Θ X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

P :

Measure (X × Y)

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

θhat :

Θ

hmem :

θhat ∈ M.paramSet

hfinite :

∀ θ ∈ M.paramSet, HasFinitePopulationRisk loss P (M.predict θ)

h :

IsMinOn (fun θ => populationRiskP M loss P θ) M.paramSet θhat

conclusion

IsPopulationRiskMinimizer (imageClass M hmeas) loss P (M.predict θhat) where mem

Proof (Lean source)

theorem populationTarget_pushforward {Θ X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (loss : Loss Y) (P : Measure (X × Y)) (hmeas : ∀ θ ∈ M.paramSet, Measurable (M.predict θ)) {θhat : Θ} (hmem : θhat ∈ M.paramSet) (hfinite : ∀ θ ∈ M.paramSet, HasFinitePopulationRisk loss P (M.predict θ)) (h : IsMinOn (fun θ => populationRiskP M loss P θ) M.paramSet θhat) : IsPopulationRiskMinimizer (imageClass M hmeas) loss P (M.predict θhat) where mem := ⟨θhat, hmem, rfl⟩ finite_self := hfinite θhat hmem finite_competitor := by rintro g ⟨θ, hθ, rfl⟩ exact hfinite θ hθ isMin := by rw [isMinOn_iff] rintro g ⟨θ, hθ, rfl⟩ simpa [populationRiskP] using (isMinOn_iff.mp h) θ hθ

Causalean.ML.populationTarget_pushforward · Causalean/ML/Core/Bridge.lean:52 · uses HasFinitePopulationRisk , IsPopulationRiskMinimizer , Loss , Predictor , imageClass , populationRiskP

1 supporting declaration (lemmas, instances)

isERMP_to_extensional theorem — A parametric empirical-risk minimizer pushes forward to an extensional empirical-risk minimizer over the realized hypothesis class.

hypotheses

ι Θ X Y :

Type*
Fintype ι
Nonempty ι
MeasurableSpace X
MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

θhat :

Θ

h :

IsERMP (empiricalRiskP M loss S) M.paramSet θhat

conclusion

IsERM (imageClass M hmeas) loss S (M.predict θhat) where mem

Proof (Lean source)

theorem isERMP_to_extensional {ι Θ X Y : Type*} [Fintype ι] [Nonempty ι] [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (loss : Loss Y) (S : ι → X × Y) (hmeas : ∀ θ ∈ M.paramSet, Measurable (M.predict θ)) {θhat : Θ} (h : IsERMP (empiricalRiskP M loss S) M.paramSet θhat) : IsERM (imageClass M hmeas) loss S (M.predict θhat) where mem := ⟨θhat, h.mem, rfl⟩ isMin := by rw [isMinOn_iff] rintro g ⟨θ, hθ, rfl⟩ simpa [empiricalRiskP] using (isMinOn_iff.mp h.isMin) θ hθ

Causalean.ML.isERMP_to_extensional · Causalean/ML/Core/Bridge.lean:38

Convex 2 core · 5 supporting Reusable convexity, existence, first-order-optimality and subgradient facts that the convex methods (logistic regression, lasso, generic convex ERM) instantiate. ★ exists_isMinOn_univ_of_coercive

Convex-analysis substrate for ERM

Reusable convexity, existence, first-order-optimality and subgradient facts that the convex methods (logistic regression, lasso, generic convex ERM) instantiate. This file is method-agnostic: it speaks only about an abstract objective on a real vector / inner-product / normed space.

theorem exists_isMinOn_univ_of_coercive reviewed

Causalean.ML

Existence via coercivity. On a proper normed real vector space, if the objective function is continuous and it tends to infinity along the cocompact filter, i.e. it is coercive — it grows without bound as the argument leaves every compact set, then a global minimizer of the objective over the whole space exists.

Formal statement

hypotheses

E :

Type u_1

E → ℝ

shared

hcont :

Continuous objective

hcoer :

Tendsto objective (cocompact E) atTop

conclusion

∃ a, IsMinOn objective univ a

Proof (Lean source)

theorem exists_isMinOn_univ_of_coercive {objective : E → ℝ} (hcont : Continuous objective) (hcoer : Tendsto objective (cocompact E) atTop) : ∃ a, IsMinOn objective univ a := by have _ : ProperSpace E := inferInstance obtain ⟨a, ha⟩ := hcont.exists_forall_le hcoer exact ⟨a, isMinOn_univ_iff.2 ha⟩

Causalean.ML.exists_isMinOn_univ_of_coercive · Causalean/ML/Core/Convex.lean:95

def SubgradientAt reviewed

Causalean.ML

A vector is a relative subgradient when the point lies in the set and the vector supports an affine minorant on that set. The definition applies to the function and constraint set at the vector and evaluation point in a real inner-product space.

Definition (Lean source)

parameters

E :

Type u_1

shared

f :

E → ℝ

s :

Set E

g x :

E

def

SubgradientAt f s g x :

Prop

given by

clause 1

x ∈ s

clause 2

y ∈ s :

f x + inner ℝ g (y - x) ≤ f y

Causalean.ML.SubgradientAt · Causalean/ML/Core/Convex.lean:125

5 supporting declarations (lemmas, instances)

empiricalRiskP_convexOn_of_loss_convex theorem — If every per-sample parameter loss is convex on Θset, so is the empirical risk of the predictor.

hypotheses

ι :

Type u_1
shared

Θ :

Type u_2
shared

X :

Type u_3
shared

Y :

Type u_4
shared

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

Θset :

Set Θ

hconv :

Convex ℝ Θset

hloss :

∀ i, ConvexOn ℝ Θset (fun θ => loss (M.predict θ (S i).1) (S i).2)

conclusion

ConvexOn ℝ Θset (empiricalRiskP M loss S)

Proof (Lean source)

theorem empiricalRiskP_convexOn_of_loss_convex (M : Predictor Θ X Y) (loss : Loss Y) (S : ι → X × Y) (Θset : Set Θ) (hconv : Convex ℝ Θset) (hloss : ∀ i, ConvexOn ℝ Θset (fun θ => loss (M.predict θ (S i).1) (S i).2)) : ConvexOn ℝ Θset (empiricalRiskP M loss S) := by unfold empiricalRiskP empiricalRisk have hsum : ConvexOn ℝ Θset (fun θ => ∑ i, loss (M.predict θ (S i).1) (S i).2) := by classical have hfin : ∀ t : Finset ι, ConvexOn ℝ Θset (fun θ => t.sum (fun i => loss (M.predict θ (S i).1) (S i).2)) := by intro t induction t using Finset.induction_on with | empty => simpa using (convexOn_const (𝕜 := ℝ) (E := Θ) (β := ℝ) (s := Θset) (0 : ℝ) hconv) | insert i t hi ht => have hadd := (hloss i).add ht have hfun : ((fun θ => loss (M.predict θ (S i).1) (S i).2) + fun θ => t.sum (fun i => loss (M.predict θ (S i).1) (S i).2)) = fun θ => (insert i t).sum (fun i => loss (M.predict θ (S i).1) (S i).2) := by funext θ simp [Finset.sum_insert hi] rwa [hfun] at hadd simpa using hfin univ simpa [smul_eq_mul] using hsum.smul (inv_nonneg.mpr (Nat.cast_nonneg (card ι)))

Causalean.ML.empiricalRiskP_convexOn_of_loss_convex · Causalean/ML/Core/Convex.lean:31
convexOn_comp_inner theorem — A convex scalar function precomposed with the linear score θ ↦ ⟪θ, x⟫ is convex. This is the workhorse turning convexity of a margin loss into convexity of the parameter objective.

hypotheses

E :

Type u_1
shared

φ :

ℝ → ℝ

hφ :

ConvexOn ℝ univ φ

x :

E

conclusion

ConvexOn ℝ univ (fun θ : E => φ (inner ℝ θ x))

Proof (Lean source)

theorem convexOn_comp_inner {φ : ℝ → ℝ} (hφ : ConvexOn ℝ univ φ) (x : E) : ConvexOn ℝ univ (fun θ : E => φ (inner ℝ θ x)) := by simpa [Function.comp_def, innerSL_apply_apply, real_inner_comm] using hφ.comp_linearMap ((innerSL ℝ x).toLinearMap)

Causalean.ML.convexOn_comp_inner · Causalean/ML/Core/Convex.lean:68
exists_isMinOn_of_isCompact theorem — Existence of a minimizer on a nonempty compact set (Weierstrass).

hypotheses

Θ :

Type u_1
Θ → ℝ
Set Θ
shared

hne :

Θset.Nonempty

hcompact :

IsCompact Θset

hcont :

ContinuousOn objective Θset

conclusion

∃ θhat ∈ Θset, IsMinOn objective Θset θhat

Proof (Lean source)

theorem exists_isMinOn_of_isCompact {objective : Θ → ℝ} {Θset : Set Θ} (hne : Θset.Nonempty) (hcompact : IsCompact Θset) (hcont : ContinuousOn objective Θset) : ∃ θhat ∈ Θset, IsMinOn objective Θset θhat := by exact hcompact.exists_isMinOn hne hcont

Causalean.ML.exists_isMinOn_of_isCompact · Causalean/ML/Core/Convex.lean:82
fderiv_eq_zero_of_isMinOn_univ theorem — First-order optimality on the whole space: at an unconstrained minimizer the Fréchet derivative vanishes.

hypotheses

E :

Type u_1
E → ℝ
E →L[ℝ] ℝ
E
shared

hmin :

IsMinOn f univ a

hderiv :

HasFDerivAt f f' a

conclusion

f' = 0

Proof (Lean source)

theorem fderiv_eq_zero_of_isMinOn_univ {f : E → ℝ} {f' : E →L[ℝ] ℝ} {a : E} (hmin : IsMinOn f univ a) (hderiv : HasFDerivAt f f' a) : f' = 0 := by exact (hmin.isLocalMin univ_mem).hasFDerivAt_eq_zero hderiv

Causalean.ML.fderiv_eq_zero_of_isMinOn_univ · Causalean/ML/Core/Convex.lean:113
subgradientAt_zero_iff_isMinOn theorem — Fermat's rule, subgradient form: 0 is a subgradient at x over s iff x minimizes f over s.

hypotheses

E :

Type u_1
E → ℝ
Set E
E
shared

hx :

x ∈ s

conclusion

SubgradientAt f s 0 x ↔ IsMinOn f s x

Proof (Lean source)

theorem subgradientAt_zero_iff_isMinOn {f : E → ℝ} {s : Set E} {x : E} (hx : x ∈ s) : SubgradientAt f s 0 x ↔ IsMinOn f s x := by constructor · intro h exact isMinOn_iff.2 fun y hy => by have := h.2 y hy simpa [SubgradientAt, inner_zero_left] using this · intro hmin refine ⟨hx, ?_⟩ intro y hy simpa [SubgradientAt, inner_zero_left] using (isMinOn_iff.1 hmin y hy)

Causalean.ML.subgradientAt_zero_iff_isMinOn · Causalean/ML/Core/Convex.lean:134

PopulationTarget 2 core · 2 supporting This file collects reusable statements about what a population-risk minimizer recovers. ★ IsResidualOrthogonal★ square_loss_population_target_of_isResidualOrthogonal

Population-risk targets

This file collects reusable statements about what a population-risk minimizer recovers. populationRisk_eq_of_both_minimizers shows that any two minimizers attain the same risk, while populationRisk_minimizer_eq_target turns a unique target minimizer into equality of functions. For squared loss, IsResidualOrthogonal records a conditional-mean normal equation, and square_loss_population_target_of_isResidualOrthogonal proves that a function satisfying it minimizes squared population risk. The conditional-expectation bridge is isolated in ML/CausalApplication/RegressionBridge.lean, so this layer stays self-contained and causal-free.

def IsResidualOrthogonal reviewed

Causalean.ML

A candidate regression function is residual-orthogonal under a joint covariate--response law precisely when its residual is orthogonal to every admissible covariate function.

Definition (Lean source)

parameters

X :

Type u_1

shared

P :

Measure (X × ℝ)

m :

X → ℝ

g :

X → ℝ

Measurable g

Integrable (fun z => (z.2 - m z.1) * g z.1) P

def

IsResidualOrthogonal P m :

Prop

given by

∫ z, (z.2 - m z.1) * g z.1 ∂P = 0

Causalean.ML.IsResidualOrthogonal · Causalean/ML/Core/PopulationTarget.lean:51

theorem square_loss_population_target_of_isResidualOrthogonal reviewed

Causalean.ML

A residual-orthogonal candidate beats any admissible competitor in squared population risk under the joint covariate--response law. The guarantee compares it with the chosen competitor and requires residual orthogonality, measurability of both functions, finite squared risks, and an integrable cross term.

Formal statement

hypotheses

X :

Type u_1

Measure (X × ℝ)

X → ℝ

shared

hm :

IsResidualOrthogonal P m

h :

X → ℝ

hm_meas :

Measurable m

hh_meas :

Measurable h

hint_m :

HasFinitePopulationRisk squaredLoss P m

hint_h :

HasFinitePopulationRisk squaredLoss P h

hcross :

Integrable (fun z => (z.2 - m z.1) * (m z.1 - h z.1)) P

conclusion

populationRisk squaredLoss P m ≤ populationRisk squaredLoss P h

Proof (Lean source)

theorem square_loss_population_target_of_isResidualOrthogonal {P : Measure (X × ℝ)} {m : X → ℝ} (hm : IsResidualOrthogonal P m) (h : X → ℝ) (hm_meas : Measurable m) (hh_meas : Measurable h) (hint_m : HasFinitePopulationRisk squaredLoss P m) (hint_h : HasFinitePopulationRisk squaredLoss P h) (hcross : Integrable (fun z => (z.2 - m z.1) * (m z.1 - h z.1)) P) : populationRisk squaredLoss P m ≤ populationRisk squaredLoss P h := by have hint_m' : Integrable (fun z : X × ℝ => (z.2 - m z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss] using hint_m have hint_h' : Integrable (fun z : X × ℝ => (z.2 - h z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss] using hint_h have hdiff : Integrable (fun z : X × ℝ => (z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) P := hint_h'.sub hint_m' have hsq_int : Integrable (fun z : X × ℝ => (m z.1 - h z.1) ^ 2) P := by have htmp : Integrable (fun z : X × ℝ => ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) - 2 * ((z.2 - m z.1) * (m z.1 - h z.1))) P := hdiff.sub (hcross.const_mul 2) convert htmp using 1 funext z ring have horth : ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P = 0 := hm (fun x => m x - h x) (hm_meas.sub hh_meas) hcross have hdiff_nonneg : 0 ≤ ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by calc 0 ≤ ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by exact integral_nonneg (fun z => sq_nonneg _) _ = 2 * ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P + ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by simp [horth] _ = ∫ z, 2 * ((z.2 - m z.1) * (m z.1 - h z.1)) + (m z.1 - h z.1) ^ 2 ∂P := by rw [integral_add] · rw [integral_const_mul] · exact hcross.const_mul 2 · exact hsq_int _ = ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by apply integral_congr_ae filter_upwards with z ring have hle : ∫ z, (z.2 - m z.1) ^ 2 ∂P ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P := by have hnonneg_sub : 0 ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P - ∫ z, (z.2 - m z.1) ^ 2 ∂P := by rw [← integral_sub hint_h' hint_m'] exact hdiff_nonneg linarith simpa [populationRisk, squaredLoss] using hle

Causalean.ML.square_loss_population_target_of_isResidualOrthogonal · Causalean/ML/Core/PopulationTarget.lean:62 · uses HasFinitePopulationRisk , IsResidualOrthogonal , populationRisk , squaredLoss

2 supporting declarations (lemmas, instances)

populationRisk_eq_of_both_minimizers theorem — Any two population-risk minimizers over the same class attain the same risk.

hypotheses

X :

Type u_1
shared

Y :

Type u_2
HypothesisClass X Y
Loss Y
Measure (X × Y)
X → Y
shared

H1 :

IsPopulationRiskMinimizer H loss P h₁

H2 :

IsPopulationRiskMinimizer H loss P h₂

conclusion

populationRisk loss P h₁ = populationRisk loss P h₂

Proof (Lean source)

theorem populationRisk_eq_of_both_minimizers {H : HypothesisClass X Y} {loss : Loss Y} {P : Measure (X × Y)} {h₁ h₂ : X → Y} (H1 : IsPopulationRiskMinimizer H loss P h₁) (H2 : IsPopulationRiskMinimizer H loss P h₂) : populationRisk loss P h₁ = populationRisk loss P h₂ := le_antisymm ((isMinOn_iff.mp H1.isMin) h₂ H2.mem) ((isMinOn_iff.mp H2.isMin) h₁ H1.mem)

Causalean.ML.populationRisk_eq_of_both_minimizers · Causalean/ML/Core/PopulationTarget.lean:32
populationRisk_minimizer_eq_target theorem — If a target is known to be the unique population-risk minimizer, every population-risk minimizer equals it.

hypotheses

X :

Type u_1
shared

Y :

Type u_2
HypothesisClass X Y
Loss Y
Measure (X × Y)
X → Y
shared

hStar :

IsPopulationRiskMinimizer H loss P hstar

hTarget :

IsPopulationRiskMinimizer H loss P target

hUnique :

∀ h₁ h₂
if
IsPopulationRiskMinimizer H loss P h₁
and
IsPopulationRiskMinimizer H loss P h₂
then
h₁ = h₂

conclusion

hstar = target

Proof (Lean source)

theorem populationRisk_minimizer_eq_target {H : HypothesisClass X Y} {loss : Loss Y} {P : Measure (X × Y)} {target hstar : X → Y} (hStar : IsPopulationRiskMinimizer H loss P hstar) (hTarget : IsPopulationRiskMinimizer H loss P target) (hUnique : ∀ h₁ h₂, IsPopulationRiskMinimizer H loss P h₁ → IsPopulationRiskMinimizer H loss P h₂ → h₁ = h₂) : hstar = target := hUnique hstar target hStar hTarget

Causalean.ML.populationRisk_minimizer_eq_target · Causalean/ML/Core/PopulationTarget.lean:40

Rate 2 core · 2 supporting The causal-free common currency between the method folders (which prove per-method L²-estimation rates) and ML/CausalApplication (which assembles them to discharge DML's nuisance-rate conditions). ★ isLittleOp_mul_quarter★ AchievesL2Rate

Learning-rate abstraction and rate algebra

The causal-free common currency between the method folders (which prove per-method L²-estimation rates) and ML/CausalApplication (which assembles them to discharge DML's nuisance-rate conditions).

* AchievesL2Rate ĥ h⋆ P rₙ μ — every L² seminorm of the estimation error is finite, and its real-number conversion is O_p(rₙ) under the experiment law. * generic probabilistic stochastic-order facts: an o_p(rₙ) with rₙ ≤ 1 is o_p(1); a product of two o_p(n^{-1/4}) is o_p(n^{-1/2}); and an O_p(n^{-1/2}) rate is o_p(n^{-1/4}) (turning a method's root-n IsBigOp into the o_p(n^{-1/4}) the DML side consumes).

theorem isLittleOp_mul_quarter reviewed

Causalean.ML

The n^{-1/4} product rule. If the sequence Xn is o_p(n^{-1/4}) and the sequence Yn is o_p(n^{-1/4}) under the probability law μ, then their pointwise product Xn·Yn is o_p(n^{-1/2}) — the DML product-rate condition from per-nuisance n^{-1/4} rates.

Formal statement

hypotheses

Ω :

Type u_1

Measure Ω

ℕ → Ω → ℝ

shared

hX :

IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

hY :

IsLittleOp Yn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

conclusion

IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ

Proof (Lean source)

theorem isLittleOp_mul_quarter (hX : IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) (hY : IsLittleOp Yn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) : IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by intro ε hε let δ : ℝ := Real.sqrt ε have hδpos : 0 < δ := Real.sqrt_pos.2 hε have hδsq : δ * δ = ε := by simpa [δ, pow_two] using Real.sq_sqrt (le_of_lt hε) let A : ℕ → Set Ω := fun n => {ω | δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) ≤ |Xn n ω * Yn n ω|} have hAt : Tendsto (fun n => μ (A n)) atTop (𝓝 0) := by simpa [A, δ] using hX δ hδpos have hBt : Tendsto (fun n => μ (B n)) atTop (𝓝 0) := by simpa [B, δ] using hY δ hδpos have hsum : Tendsto (fun n => μ (A n) + μ (B n)) atTop (𝓝 0) := by simpa using hAt.add hBt refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hsum (Eventually.of_forall fun n => zero_le) ?_ filter_upwards [eventually_ge_atTop 1] with n hn have hnpos : 0 < (n : ℝ) := by exact_mod_cast hn have hrate_prod : (n : ℝ) ^ (-(1 / 4 : ℝ)) * (n : ℝ) ^ (-(1 / 4 : ℝ)) = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [← Real.rpow_add hnpos] congr 1 norm_num have hpoint : μ (C n) ≤ μ (A n) + μ (B n) := by have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ |Yn n ω| := by intro hy exact hnot (inr hy) have hXlt : |Xn n ω| < δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := lt_of_not_ge hnotA have hYlt : |Yn n ω| < δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := lt_of_not_ge hnotB have hprod : |Xn n ω * Yn n ω| < ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by calc |Xn n ω * Yn n ω| = |Xn n ω| * |Yn n ω| := abs_mul (Xn n ω) (Yn n ω) _ < (δ * (n : ℝ) ^ (-(1 / 4 : ℝ))) * (δ * (n : ℝ) ^ (-(1 / 4 : ℝ))) := mul_lt_mul'' hXlt hYlt (abs_nonneg _) (abs_nonneg _) _ = ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [mul_mul_mul_comm, hδsq, hrate_prod] exact (not_lt_of_ge hω) hprod calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) simpa [C] using hpoint

Causalean.ML.isLittleOp_mul_quarter · Causalean/ML/Core/Rate.lean:47 · uses IsLittleOp

def AchievesL2Rate reviewed

Causalean.ML

Achieving an L² estimation rate means that experiment-indexed regression estimates approach a target under a joint law with finite L² error everywhere, and that those errors are stochastically bounded by the claimed rate under the experiment law at the supplied rate sequence.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type*

MeasurableSpace X

hhat :

ℕ → Ω → (X → ℝ)

hstar :

X → ℝ

P :

Measure (X × ℝ)

rn :

ℕ → ℝ

μ :

Measure Ω

def

AchievesL2Rate hhat hstar P rn μ :

Prop

given by

clause 1

n ω :

eLpNorm (fun x => hhat n ω x - hstar x) 2 (P.map fst) ≠ ⊤

clause 2

IsBigOp (fun n ω => (eLpNorm (fun x => hhat n ω x - hstar x) 2 (P.map fst)).toReal) rn μ

Causalean.ML.AchievesL2Rate · Causalean/ML/Core/Rate.lean:183

2 supporting declarations (lemmas, instances)

isLittleOp_one_of_le_one theorem — Rate weakening: an o_p(rn) sequence with rn ≤ 1 is o_p(1).

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

rn :

ℕ → ℝ

hr :

∀ n, rn n ≤ 1

h :

IsLittleOp Xn rn μ

conclusion

IsLittleOp Xn (fun _ => 1) μ

Proof (Lean source)

theorem isLittleOp_one_of_le_one {rn : ℕ → ℝ} (hr : ∀ n, rn n ≤ 1) (h : IsLittleOp Xn rn μ) : IsLittleOp Xn (fun _ => 1) μ := by intro ε hε have hlim : Tendsto (fun n => μ {ω | ε * rn n ≤ |Xn n ω|}) atTop (𝓝 0) := h ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hlim (fun n => zero_le) ?_ intro n apply measure_mono intro ω hω have hmul : ε * rn n ≤ ε * 1 := mul_le_mul_of_nonneg_left (hr n) (le_of_lt hε) exact hmul.trans (by simpa using hω)

Causalean.ML.isLittleOp_one_of_le_one · Causalean/ML/Core/Rate.lean:33
isLittleOp_quarter_of_isBigOp_sqrt theorem — An O_p(n^{-1/2}) (root-n) rate is o_p(n^{-1/4}): a method's root-n estimation rate clears the DML o_p(n^{-1/4}) bar.

hypotheses

Ω :

Type u_1
Measure Ω
ℕ → Ω → ℝ
shared

h :

IsBigOp Xn (fun n => (sqrt (n : ℝ))⁻¹) μ

conclusion

IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

Proof (Lean source)

theorem isLittleOp_quarter_of_isBigOp_sqrt (h : IsBigOp Xn (fun n => (sqrt (n : ℝ))⁻¹) μ) : IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hhalfpos : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num) rcases h (δ / 2) hhalfpos with ⟨M0, hM0pos, hM0⟩ let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | M * (sqrt (n : ℝ))⁻¹ ≤ |Xn n ω|} have hhalf_lt : δ / 2 < δ := ENNReal.half_lt_self hδ.ne' hδtop have hBevent : ∀ᶠ n : ℕ in atTop, μ (B n) < δ := by filter_upwards [hM0] with n hn have hrate_nonneg : 0 ≤ (sqrt (n : ℝ))⁻¹ := inv_nonneg.mpr (Real.sqrt_nonneg _) have hsubset : B n ⊆ {ω | M0 * (sqrt (n : ℝ))⁻¹ ≤ |Xn n ω|} := by intro ω hω exact (mul_le_mul_of_nonneg_right hM0le hrate_nonneg).trans hω exact (le_trans (measure_mono hsubset) hn).trans_lt hhalf_lt have hthreshold : ∀ᶠ n : ℕ in atTop, M * (sqrt (n : ℝ))⁻¹ ≤ ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) := by have ht : Tendsto (fun n : ℕ => (M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ))) atTop (𝓝 0) := by have hp : Tendsto (fun x : ℝ => x ^ (-(1 / 4 : ℝ))) atTop (𝓝 0) := by exact tendsto_rpow_neg_atTop (by norm_num : (0 : ℝ) < (1 / 4 : ℝ)) simpa using (Tendsto.const_mul (M / ε) (hp.comp tendsto_natCast_atTop_atTop)) have hevent_abs : ∀ᶠ n : ℕ in atTop, |(M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ))| < 1 := by have hnear := (Metric.tendsto_nhds.mp ht) 1 (by norm_num : (0 : ℝ) < (1 : ℝ)) simpa [Real.dist_eq, abs_mul, abs_div] using hnear filter_upwards [hevent_abs, eventually_ge_atTop 1] with n hnabs hn_ge have hnsmall : (M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ)) < 1 := (abs_lt.mp hnabs).2 have hnpos : 0 < (n : ℝ) := by exact_mod_cast hn_ge let q : ℝ := (n : ℝ) ^ (-(1 / 4 : ℝ)) have hqpos : 0 < q := by dsimp [q] exact Real.rpow_pos_of_pos hnpos _ have hinv_eq : (sqrt (n : ℝ))⁻¹ = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [Real.sqrt_eq_rpow] rw [← Real.rpow_neg (le_of_lt hnpos)] have hpow_add : q * q = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by dsimp [q] rw [← Real.rpow_add hnpos] congr 1 norm_num have hmul : (M / ε * q) * (ε * q) ≤ 1 * (ε * q) := by exact mul_le_mul_of_nonneg_right (le_of_lt hnsmall) (le_of_lt (mul_pos hε hqpos)) have hleft : (M / ε * q) * (ε * q) = M * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [← hpow_add] field_simp [hε.ne'] calc M * (sqrt (n : ℝ))⁻¹ = M * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [hinv_eq] _ = (M / ε * q) * (ε * q) := by rw [hleft] _ ≤ 1 * (ε * q) := hmul _ = ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) := by simp [q] filter_upwards [hBevent, hthreshold] with n hBn hthr have hsubset : A n ⊆ B n := by intro ω hω dsimp [A, B] at hω ⊢ exact hthr.trans hω calc μ {ω | ε * (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) n ≤ ‖Xn n ω‖} = μ (A n) := by congr 1 _ ≤ δ := le_of_lt (lt_of_le_of_lt (measure_mono hsubset) hBn)

Causalean.ML.isLittleOp_quarter_of_isBigOp_sqrt · Causalean/ML/Core/Rate.lean:106