Fill auxiliary sorries in Cor 11.10.3 and Prop 11.10.6

[XPiPiT]

Scope

This PR fills only the two unlabeled auxiliary sorries in Analysis/Section_11_10.lean:

• RS_integ_eq_integ_of_mul_deriv (Corollary 11.10.3): the two why sub-lemmas inside h1 and h2.
• RS_integ_of_comp (Proposition 11.10.6): the hfφ_bdd step.

Exercise-labeled sorries are intentionally untouched, in respect of the policy stated in CONTRIBUTING.md ("I do not intend to place solutions in this repository directly"):

• integ_of_mul_deriv (Exercise 11.10.1) — unchanged
• PiecewiseConstantOn.RS_integ_of_comp (Exercise 11.10.2) — unchanged
• the bottom example (Exercise 11.10.3) — unchanged

The interpretation here is that the unlabeled sorries inside otherwise-complete proofs (those with the comment -- This proof is adapted from the structure of the original text) are completion gaps in the proof scaffolding, not exercises for the reader. If this interpretation is wrong and these are also intended as exercises, please feel free to close.

Approach

Cor 11.10.3 — both why sub-lemmas

Both have the same shape (lower vs. upper integral monotonicity under non-negative weight multiplication). For each:

• Pick a piecewise-constant minorant/majorant g of h * α'.
• Use h ≤ f (resp. f ≤ h) and α' ≥ 0 (from the existing hα'_nonneg) to lift g to a minorant/majorant of f * α' via mul_le_mul_of_nonneg_right.
• Conclude via integ_le_lower_integral / upper_integral_le_integ.

The BddOn (h * α') step is inlined as a 4-line direct proof rather than depending on BddOn.mul (which is sorry in Section_9_6.lean:185), keeping the chain free of unproved dependencies.

Prop 11.10.6 — hfφ_bdd

Boundedness of f ∘ φ follows immediately from boundedness of f on [φ a, φ b] plus φ([a,b]) ⊆ [φ a, φ b] from monotonicity. The same upper bound transfers without modification.

Build status

lake build passes with zero errors (verified locally; 3533 jobs built successfully).

Notes

• No other files modified.
• All Exercise sorries left intact.
• Happy to revise scope or close if any of this conflicts with the project's intent.